:: ZF_REFLE semantic presentation

REAL is set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty V35() cardinal limit_cardinal countable denumerable Element of K40(REAL)
K40(REAL) is non empty set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty V35() cardinal limit_cardinal countable denumerable set
K40(NAT) is non empty V35() set
K40(NAT) is non empty V35() set
VAR is non empty countable Element of K40(NAT)
5 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT : 5 <= b₁ } is set
K40(VAR) is non empty set
{} is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V16() empty V20() Function-like one-to-one constant functional V35() cardinal {} -element Cardinal-yielding countable set
the Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V16() empty V20() Function-like one-to-one constant functional V35() cardinal {} -element Cardinal-yielding countable set is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V16() empty V20() Function-like one-to-one constant functional V35() cardinal {} -element Cardinal-yielding countable set
1 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
0 is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V16() empty V20() Function-like one-to-one constant functional V35() cardinal {} -element Cardinal-yielding countable Element of NAT
the_axiom_of_pairs is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
x. 0 is Element of VAR
5 + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
x. 1 is Element of VAR
5 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
x. 2 is Element of VAR
5 + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
x. 3 is Element of VAR
5 + 3 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
(x. 3) 'in' (x. 2) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K210(NAT,1) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K219((x. 3)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,1),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K219((x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K210(NAT,0) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,0),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K219((x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) '=' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K219((x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 3) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K210(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((x. 3) '=' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K210(NAT,3) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,3),('not' ((x. 3) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),('not' ((x. 3) '=' (x. 0)))),('not' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))),('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 3) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))),('not' ((x. 3) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) '&' ((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))),((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
4 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
K210(NAT,4) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),(x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
the_axiom_of_unions is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
(x. 2) 'in' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,1),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 2) 'in' (x. 3) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 3))),((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))),('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))),('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) '&' ((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))),((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
the_axiom_of_infinity is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
(x. 1) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,1),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 1))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 2) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) '=' (x. 2) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((x. 3) '=' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) '=' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 0))),('not' ((x. 3) '=' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
x. 4 is Element of VAR
5 + 4 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
(x. 4) 'in' (x. 2) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K219((x. 4)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,1),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 4))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 4) 'in' (x. 3) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 4))),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) 'in' (x. 3)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) 'in' (x. 2))),('not' ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))))),(All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 0))),('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 1) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 1) 'in' (x. 0))),(All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 0),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
the_axiom_of_power_sets is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 3) 'in' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))),('not' ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))),('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))) '&' ((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))),((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
{(x. 0),(x. 1),(x. 2)} is non empty set
(x. 4) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,0),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 4))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Element of M
M is Element of M
{L,M} is non empty Element of M
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Element of M
union L is Element of M
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Element of M
M is Element of M
H is Element of M
phi is epsilon-transitive epsilon-connected ordinal set
succ phi is epsilon-transitive epsilon-connected ordinal non empty set
{phi} is non empty trivial 1 -element set
phi \/ {phi} is non empty set
a is Element of M
f is Element of M
M is Element of M
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Element of M
bool L is non empty Element of M
M /\ (bool L) is set
M is epsilon-transitive non empty subset-closed Tarski universal set
K41(VAR,M) is Relation-like non empty set
K40(K41(VAR,M)) is non empty set
L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
Free L is V35() countable Element of K40(VAR)
L <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
L => ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
L '&' ('not' ((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),L),('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (L '&' ('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(L '&' ('not' ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) => L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) '&' ('not' L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))),('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) '=' (x. 0)) '&' ('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) '=' (x. 0)) '&' ('not' L))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(L => ((x. 4) '=' (x. 0))) '&' (((x. 4) '=' (x. 0)) => L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))),(((x. 4) '=' (x. 0)) => L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
M is Relation-like VAR -defined M -valued Function-like quasi_total Element of K40(K41(VAR,M))
def_func' (L,M) is Relation-like M -defined M -valued Function-like quasi_total Element of K40(K41(M,M))
K41(M,M) is Relation-like non empty set
K40(K41(M,M)) is non empty set
H is Element of M
(def_func' (L,M)) .: H is Element of K40(M)
K40(M) is non empty set
card H is epsilon-transitive epsilon-connected ordinal cardinal set
card M is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card ((def_func' (L,M)) .: H) is epsilon-transitive epsilon-connected ordinal cardinal set
L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
Free L is V35() countable Element of K40(VAR)
the_axiom_of_substitution_for L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
L <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
L => ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
L '&' ('not' ((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),L),('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (L '&' ('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(L '&' ('not' ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) => L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) '&' ('not' L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))),('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) '=' (x. 0)) '&' ('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) '=' (x. 0)) '&' ('not' L))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(L => ((x. 4) '=' (x. 0))) '&' (((x. 4) '=' (x. 0)) => L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))),(((x. 4) '=' (x. 0)) => L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) 'in' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 1)) '&' L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (