:: ZFMODEL2 semantic presentation

REAL is set
NAT is non empty V19() V20() V21() Element of K27(REAL)
K27(REAL) is set
NAT is non empty V19() V20() V21() set
K27(NAT) is set
K27(NAT) is set
VAR is non empty Element of K27(NAT)
K27(VAR) is set
1 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
2 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
3 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
0 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
the Function-like functional empty ext-real non positive non negative V18() V19() V20() V21() V23() V24() V25() V26() finite V37() V43() set is Function-like functional empty ext-real non positive non negative V18() V19() V20() V21() V23() V24() V25() V26() finite V37() V43() set
{} is set
x. 0 is Element of VAR
x. 3 is Element of VAR
4 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
x. 4 is Element of VAR
(x. 4) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
{(x. 3),(x. 4)} is finite set
{0,1,2,3,4} is finite set
M is Element of VAR
{M} is finite set
H is Element of VAR
{H} is finite set
i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
i / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (i / (M,H)) is Element of K27(VAR)
Free i is Element of K27(VAR)
(Free i) \ {M} is Element of K27(VAR)
((Free i) \ {M}) \/ {H} is set
v is Element of VAR
a is Element of VAR
v '=' a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(v '=' a) / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v '=' a) / (M,H)) is Element of K27(VAR)
Free (v '=' a) is Element of K27(VAR)
(Free (v '=' a)) \ {M} is Element of K27(VAR)
((Free (v '=' a)) \ {M}) \/ {H} is set
v 'in' a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(v 'in' a) / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v 'in' a) / (M,H)) is Element of K27(VAR)
Free (v 'in' a) is Element of K27(VAR)
(Free (v 'in' a)) \ {M} is Element of K27(VAR)
((Free (v 'in' a)) \ {M}) \/ {H} is set
m4 is Element of VAR
f is Element of VAR
{m4,f} is finite set
{v,a} is finite set
{v,a} \ {M} is finite Element of K27({v,a})
K27({v,a}) is finite V37() set
({v,a} \ {M}) \/ {H} is finite set
p is set
m4 'in' f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
m4 '=' f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (v / (M,H)) is Element of K27(VAR)
Free v is Element of K27(VAR)
(Free v) \ {M} is Element of K27(VAR)
((Free v) \ {M}) \/ {H} is set
a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (a / (M,H)) is Element of K27(VAR)
Free a is Element of K27(VAR)
(Free a) \ {M} is Element of K27(VAR)
((Free a) \ {M}) \/ {H} is set
v '&' a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(v '&' a) / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v '&' a) / (M,H)) is Element of K27(VAR)
Free (v '&' a) is Element of K27(VAR)
(Free (v '&' a)) \ {M} is Element of K27(VAR)
((Free (v '&' a)) \ {M}) \/ {H} is set
(v / (M,H)) '&' (a / (M,H)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v / (M,H)) '&' (a / (M,H))) is Element of K27(VAR)
(Free (v / (M,H))) \/ (Free (a / (M,H))) is Element of K27(VAR)
(((Free v) \ {M}) \/ {H}) \/ (((Free a) \ {M}) \/ {H}) is set
(Free v) \/ (Free a) is Element of K27(VAR)
((Free v) \/ (Free a)) \ {M} is Element of K27(VAR)
(((Free v) \/ (Free a)) \ {M}) \/ {H} is set
m4 is set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (v / (M,H)) is Element of K27(VAR)
Free v is Element of K27(VAR)
(Free v) \ {M} is Element of K27(VAR)
((Free v) \ {M}) \/ {H} is set
a is Element of VAR
All (a,v) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(All (a,v)) / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((All (a,v)) / (M,H)) is Element of K27(VAR)
Free (All (a,v)) is Element of K27(VAR)
(Free (All (a,v))) \ {M} is Element of K27(VAR)
((Free (All (a,v))) \ {M}) \/ {H} is set
{a} is finite set
(Free v) \ {a} is Element of K27(VAR)
m4 is Element of VAR
{m4} is finite set
(((Free v) \ {M}) \/ {H}) \ {m4} is Element of K27((((Free v) \ {M}) \/ {H}))
K27((((Free v) \ {M}) \/ {H})) is set
((Free v) \ {a}) \ {M} is Element of K27(VAR)
(((Free v) \ {a}) \ {M}) \/ {H} is set
f is set
(Free (v / (M,H))) \ {m4} is Element of K27(VAR)
All (m4,(v / (M,H))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (All (m4,(v / (M,H)))) is Element of K27(VAR)
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (v / (M,H)) is Element of K27(VAR)
Free v is Element of K27(VAR)
(Free v) \ {M} is Element of K27(VAR)
((Free v) \ {M}) \/ {H} is set
'not' v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
('not' v) / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (('not' v) / (M,H)) is Element of K27(VAR)
Free ('not' v) is Element of K27(VAR)
(Free ('not' v)) \ {M} is Element of K27(VAR)
((Free ('not' v)) \ {M}) \/ {H} is set
'not' (v / (M,H)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ('not' (v / (M,H))) is Element of K27(VAR)
M is Element of VAR
{M} is finite set
H is Element of VAR
{H} is finite set
i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in i is non empty Element of K27(VAR)
Free i is Element of K27(VAR)
i / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (i / (H,M)) is Element of K27(VAR)
(Free i) \ {H} is Element of K27(VAR)
((Free i) \ {H}) \/ {M} is set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty Element of K27(VAR)
Free v is Element of K27(VAR)
v / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (v / (H,M)) is Element of K27(VAR)
(Free v) \ {H} is Element of K27(VAR)
((Free v) \ {H}) \/ {M} is set
a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in a is non empty Element of K27(VAR)
Free a is Element of K27(VAR)
a / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (a / (H,M)) is Element of K27(VAR)
(Free a) \ {H} is Element of K27(VAR)
((Free a) \ {H}) \/ {M} is set
v '&' a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (v '&' a) is non empty Element of K27(VAR)
Free (v '&' a) is Element of K27(VAR)
(v '&' a) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v '&' a) / (H,M)) is Element of K27(VAR)
(Free (v '&' a)) \ {H} is Element of K27(VAR)
((Free (v '&' a)) \ {H}) \/ {M} is set
(v / (H,M)) '&' (a / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v / (H,M)) '&' (a / (H,M))) is Element of K27(VAR)
(Free (v / (H,M))) \/ (Free (a / (H,M))) is Element of K27(VAR)
(Free v) \/ (Free a) is Element of K27(VAR)
(variables_in v) \/ (variables_in a) is Element of K27(VAR)
((Free v) \ {H}) \/ ((Free a) \ {H}) is Element of K27(VAR)
(((Free v) \ {H}) \/ ((Free a) \ {H})) \/ {M} is set
{M} \/ ((Free v) \ {H}) is set
({M} \/ ((Free v) \ {H})) \/ ((Free a) \ {H}) is set
(({M} \/ ((Free v) \ {H})) \/ ((Free a) \ {H})) \/ {M} is set
{M} \/ (((Free v) \ {H}) \/ ((Free a) \ {H})) is set
({M} \/ (((Free v) \ {H}) \/ ((Free a) \ {H}))) \/ {M} is set
(((Free (v '&' a)) \ {H}) \/ {M}) \/ {M} is set
{M} \/ {M} is finite set
((Free (v '&' a)) \ {H}) \/ ({M} \/ {M}) is set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty Element of K27(VAR)
Free v is Element of K27(VAR)
v / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (v / (H,M)) is Element of K27(VAR)
(Free v) \ {H} is Element of K27(VAR)
((Free v) \ {H}) \/ {M} is set
a is Element of VAR
All (a,v) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (All (a,v)) is non empty Element of K27(VAR)
Free (All (a,v)) is Element of K27(VAR)
(All (a,v)) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((All (a,v)) / (H,M)) is Element of K27(VAR)
(Free (All (a,v))) \ {H} is Element of K27(VAR)
((Free (All (a,v))) \ {H}) \/ {M} is set
{a} is finite set
(Free v) \ {a} is Element of K27(VAR)
f is Element of VAR
All (f,(v / (H,M))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (All (f,(v / (H,M)))) is Element of K27(VAR)
{f} is finite set
(Free (v / (H,M))) \ {f} is Element of K27(VAR)
(variables_in v) \/ {a} is set
p is set
p is set
p is set
((Free v) \ {a}) \/ {M} is set
p is set
((Free v) \ {a}) \ {M} is Element of K27(VAR)
v is Element of VAR
a is Element of VAR
v '=' a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (v '=' a) is non empty Element of K27(VAR)
Free (v '=' a) is Element of K27(VAR)
(v '=' a) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v '=' a) / (H,M)) is Element of K27(VAR)
(Free (v '=' a)) \ {H} is Element of K27(VAR)
((Free (v '=' a)) \ {H}) \/ {M} is set
v 'in' a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (v 'in' a) is non empty Element of K27(VAR)
Free (v 'in' a) is Element of K27(VAR)
(v 'in' a) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v 'in' a) / (H,M)) is Element of K27(VAR)
(Free (v 'in' a)) \ {H} is Element of K27(VAR)
((Free (v 'in' a)) \ {H}) \/ {M} is set
m4 is Element of VAR
f is Element of VAR
m4 '=' f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
{m4,f} is finite set
{v,a} is finite set
p is set
m4 'in' f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
p is set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty Element of K27(VAR)
Free v is Element of K27(VAR)
v / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (v / (H,M)) is Element of K27(VAR)
(Free v) \ {H} is Element of K27(VAR)
((Free v) \ {H}) \/ {M} is set
'not' v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in ('not' v) is non empty Element of K27(VAR)
Free ('not' v) is Element of K27(VAR)
('not' v) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (('not' v) / (H,M)) is Element of K27(VAR)
(Free ('not' v)) \ {H} is Element of K27(VAR)
((Free ('not' v)) \ {H}) \/ {M} is set
'not' (v / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ('not' (v / (H,M))) is Element of K27(VAR)
M is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in M is non empty Element of K27(VAR)
rng M is finite set
(rng M) \ {0,1,2,3,4} is finite Element of K27((rng M))
K27((rng M)) is finite V37() set
M is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in M is non empty finite Element of K27(VAR)
H is Element of VAR
i is Element of VAR
H '=' i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (H '=' i) is non empty finite Element of K27(VAR)
H 'in' i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (H 'in' i) is non empty finite Element of K27(VAR)
v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. v is Element of VAR
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. a is Element of VAR
a + v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
v + a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
(v + a) + 1 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
{H,i} is finite set
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. m4 is Element of VAR
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. m4 is Element of VAR
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in H is non empty finite Element of K27(VAR)
i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in i is non empty finite Element of K27(VAR)
H '&' i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (H '&' i) is non empty finite Element of K27(VAR)
v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
f is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. f is Element of VAR
(variables_in H) \/ (variables_in i) is finite Element of K27(VAR)
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in H is non empty finite Element of K27(VAR)
i is Element of VAR
All (i,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (All (i,H)) is non empty finite Element of K27(VAR)
v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. a is Element of VAR
a + 1 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
f is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. f is Element of VAR
{i} is finite set
(variables_in H) \/ {i} is finite set
a + 0 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in H is non empty finite Element of K27(VAR)
'not' H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in ('not' H) is non empty finite Element of K27(VAR)
i is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
H is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. H is Element of VAR
M is Element of VAR
H is non empty set
K28(VAR,H) is set
K27(K28(VAR,H)) is set
i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in i is non empty finite Element of K27(VAR)
All (M,i) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
Free i is Element of K27(VAR)
v . M is Element of H
v / (M,(v . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
M is Element of VAR
H is non empty set
K28(VAR,H) is set
K27(K28(VAR,H)) is set
i is Element of H
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty finite Element of K27(VAR)
a is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
a / (M,i) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
All (M,v) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a . M is Element of H
(a / (M,i)) / (M,(a . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
a / (M,(a . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
M is Element of VAR
H is Element of VAR
i is Element of VAR
v is non empty set
K28(VAR,v) is set
K27(K28(VAR,v)) is set
a is Element of v
m4 is Element of v
f is Element of v
p is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
p / (M,a) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
(p / (M,a)) / (H,m4) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
((p / (M,a)) / (H,m4)) / (i,f) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
p / (i,f) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
(p / (i,f)) / (H,m4) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
((p / (i,f)) / (H,m4)) / (M,a) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
p / (H,m4) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
(p / (H,m4)) / (i,f) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
((p / (H,m4)) / (i,f)) / (M,a) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
(p / (H,m4)) / (M,a) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
M is Element of VAR
H is Element of VAR
i is Element of VAR
v is Element of VAR
a is non empty set
K28(VAR,a) is set
K27(K28(VAR,a)) is set
m4 is Element of a
f is Element of a
p is Element of a
a is Element of a
r is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (M,m4)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (M,m4)) / (H,f)) / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (M,m4)) / (H,f)) / (i,p)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (H,f)) / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (H,f)) / (i,p)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (H,f)) / (i,p)) / (v,a)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (i,p)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (i,p)) / (v,a)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (i,p)) / (v,a)) / (M,m4)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (v,a)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (v,a)) / (H,f)) / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (v,a)) / (H,f)) / (i,p)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (M,m4)) / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (M,m4)) / (i,p)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (M,m4)) / (i,p)) / (v,a)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (H,f)) / (i,p)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (H,f)) / (i,p)) / (M,m4)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
M is Element of VAR
H is Element of VAR
i is Element of VAR
v is Element of VAR
a is non empty set
K28(VAR,a) is set
K27(K28(VAR,a)) is set
m4 is Element of a
f is Element of a
p is Element of a
a is Element of a
r is Element of a
r2 is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r2 / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r2 / (M,m4)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (M,m4)) / (H,f)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r2 / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r2 / (H,f)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (M,m4)) / (H,f)) / (i,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (M,m4)) / (H,f)) / (i,a)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r2 / (H,f)) / (i,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (H,f)) / (i,a)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (M,m4)) / (H,f)) / (i,a)) / (v,r) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((((r2 / (M,m4)) / (H,f)) / (i,a)) / (v,r)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (H,f)) / (i,a)) / (v,r) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (H,f)) / (i,a)) / (v,r)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r2 / (H,f)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (H,f)) / (M,m4)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (M,m4)) / (H,f)) / (M,p)) / (i,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (H,f)) / (M,p)) / (i,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((((r2 / (M,m4)) / (H,f)) / (i,a)) / (M,p)) / (v,r) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (H,f)) / (i,a)) / (M,p)) / (v,r) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
M is Element of VAR
H is non empty set
K28(VAR,H) is set
K27(K28(VAR,H)) is set
i is Element of H
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free v is Element of K27(VAR)
a is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
a / (M,i) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
a . M is Element of H
a / (M,(a . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
All (M,v) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(a / (M,i)) / (M,(a . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free H is Element of K27(VAR)
H <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
i is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (H,i) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
v is Element of M
(def_func' (H,i)) . v is Element of M
i / ((x. 3),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a is Element of M
(i / ((x. 3),v)) / ((x. 4),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(i / ((x. 3),v)) . (x. 3) is Element of M
m4 is Element of VAR
((i / ((x. 3),v)) / ((x. 4),a)) . m4 is Element of M
i . m4 is Element of M
(i / ((x. 3),v)) . m4 is Element of M
((i / ((x. 3),v)) / ((x. 4),a)) . (x. 3) is Element of M
((i / ((x. 3),v)) / ((x. 4),a)) . (x. 4) is Element of M
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free H is Element of K27(VAR)
H <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (H,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
i is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (H,i) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
v is Element of M
(def_func' (H,i)) . v is set
(def_func (H,M)) . v is set
(def_func' (H,i)) . v is Element of M
i / ((x. 3),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(i / ((x. 3),v)) / ((x. 4),((def_func' (H,i)) . v)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((i / ((x. 3),v)) / ((x. 4),((def_func' (H,i)) . v))) . (x. 3) is Element of M
(i / ((x. 3),v)) . (x. 3) is Element of M
((i / ((x. 3),v)) / ((x. 4),((def_func' (H,i)) . v))) . (x. 4) is Element of M
(def_func (H,M)) . v is Element of M
M is Element of VAR
H is Element of VAR
i is non empty set
K28(VAR,i) is set
K27(K28(VAR,i)) is set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty finite Element of K27(VAR)
v / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . M is Element of i
a / (H,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
m4 is Element of VAR
f is Element of VAR
m4 '=' f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (m4 '=' f) is non empty finite Element of K27(VAR)
(m4 '=' f) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
m4 'in' f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (m4 'in' f) is non empty finite Element of K27(VAR)
(m4 'in' f) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
p is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
p . M is Element of i
p / (H,(p . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a is Element of VAR
r is Element of VAR
(p / (H,(p . M))) . f is Element of i
p . r is Element of i
(p / (H,(p . M))) . m4 is Element of i
p . a is Element of i
a '=' r is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
p is Element of VAR
a is Element of VAR
r is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
r . M is Element of i
r / (H,(r . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(r / (H,(r . M))) . m4 is Element of i
r . p is Element of i
(r / (H,(r . M))) . f is Element of i
r . a is Element of i
p 'in' a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
m4 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in m4 is non empty finite Element of K27(VAR)
m4 / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in f is non empty finite Element of K27(VAR)
f / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
m4 '&' f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (m4 '&' f) is non empty finite Element of K27(VAR)
(m4 '&' f) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(variables_in m4) \/ (variables_in f) is finite Element of K27(VAR)
p is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
p . M is Element of i
p / (H,(p . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(m4 / (H,M)) '&' (f / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(m4 / (H,M)) '&' (f / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
m4 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in m4 is non empty finite Element of K27(VAR)
m4 / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
f is Element of VAR
All (f,m4) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (All (f,m4)) is non empty finite Element of K27(VAR)
(All (f,m4)) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
p is Element of VAR
{f} is finite set
(variables_in m4) \/ {f} is finite set
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . M is Element of i
a / (H,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
Free m4 is Element of K27(VAR)
All (p,(m4 / (H,M))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Element of i
a / (M,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,r)) . M is Element of i
(a / (M,r)) / (H,((a / (M,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,r)) / (H,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (H,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,r)) / (M,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
All (M,m4) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(a / (H,r)) . M is Element of i
((a / (H,r)) / (M,r)) / (M,((a / (H,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,r)) / (M,((a / (H,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
All (H,m4) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Element of i
a / (f,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (f,r)) . M is Element of i
(a / (f,r)) / (H,((a / (f,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,(a . M))) / (f,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
Free (All (f,m4)) is Element of K27(VAR)
All (H,m4) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All (M,(All (H,m4))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Element of i
a / (M,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,r)) / (H,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,r)) . M is Element of i
All (M,(m4 / (H,M))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Element of i
(a / (H,(a . M))) / (f,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (f,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (f,r)) / (H,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (f,r)) . M is Element of i
(a / (f,r)) / (H,((a / (f,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
All (f,(m4 / (H,M))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
m4 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in m4 is non empty finite Element of K27(VAR)
m4 / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
'not' m4 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in ('not' m4) is non empty finite Element of K27(VAR)
('not' m4) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
f is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
f . M is Element of i
f / (H,(f . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
'not' (m4 / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
'not' (m4 / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
M is Element of VAR
H is Element of VAR
i is non empty set
K28(VAR,i) is set
K27(K28(VAR,i)) is set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty finite Element of K27(VAR)
v / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . H is Element of i
a / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) . M is Element of i
(a / (M,(a . H))) / (H,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (H,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,(a . H))) / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
M is Element of VAR
H is Element of VAR
i is non empty set
K28(VAR,i) is set
K27(K28(VAR,i)) is set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free v is Element of K27(VAR)
v <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(v <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(v <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(v <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty finite Element of K27(VAR)
v / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (v / (H,M)) is Element of K27(VAR)
(v / (H,M)) <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),((v / (H,M)) <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),((v / (H,M)) <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),((v / (H,M)) <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . H is Element of i
a / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
def_func' (v,a) is Relation-like i -defined i -valued Function-like non empty V14(i) V30(i,i) Element of K27(K28(i,i))
K28(i,i) is set
K27(K28(i,i)) is set
def_func' ((v / (H,M)),(a / (M,(a . H)))) is Relation-like i -defined i -valued Function-like non empty V14(i) V30(i,i) Element of K27(K28(i,i))
variables_in (v / (H,M)) is non empty finite Element of K27(VAR)
{M} is finite set
{H} is finite set
(Free v) \ {H} is Element of K27(VAR)
((Free v) \ {H}) \/ {M} is set
p is Element of i
a / ((x. 3),p) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a is Element of i
(a / ((x. 3),p)) / ((x. 0),a) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) / ((x. 3),p) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((a / (M,(a . H))) / ((x. 3),p)) / ((x. 0),a) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
r2 is Element of i
((a / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(((a / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2)) . (x. 4) is Element of i
(((a / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2)) . (x. 0) is Element of i
((a / ((x. 3),p)) / ((x. 0),a)) . (x. 0) is Element of i
(((a / (M,(a . H))) / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((((a / (M,(a . H))) / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2)) . (x. 0) is Element of i
(((a / (M,(a . H))) / ((x. 3),p)) / ((x. 0),a)) . (x. 0) is Element of i
((((a / (M,(a . H))) / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2)) . (x. 4) is Element of i
(((a / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2)) / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((((a / (M,(a . H))) / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2)) . M is Element of i
((((a / (M,(a . H))) / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2)) / (H,(((((a / (M,(a . H))) / ((x. 3),p)) / ((x. 0),a)) / ((x. 4),r2)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
p is Element of i
(def_func' (v,a)) . p is set
(def_func' ((v / (H,M)),(a / (M,(a . H))))) . p is set
(def_func' (v,a)) . p is Element of i
a / ((x. 3),p) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((a / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p))) / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) / ((x. 3),p) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((a / (M,(a . H))) / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(((a / (M,(a . H))) / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p))) . H is Element of i
(((a / (M,(a . H))) / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p))) / (M,((((a / (M,(a . H))) / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p))) . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(def_func' ((v / (H,M)),(a / (M,(a . H))))) . p is Element of i
M is Element of VAR
H is Element of VAR
i is non empty set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty finite Element of K27(VAR)
v / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
K28(VAR,i) is set
K27(K28(VAR,i)) is set
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . H is Element of i
a / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) . M is Element of i
(a / (M,(a . H))) / (H,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . M is Element of i
((a / (M,(a . H))) / (H,(a . H))) / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (H,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,(a . H))) / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((a / (H,(a . H))) / (M,(a . H))) / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,(a . H))) / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
K28(VAR,i) is set
K27(K28(VAR,i)) is set
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . M is Element of i
a / (H,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
H is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free i is Element of K27(VAR)
i <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(i <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(i <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(i <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (i,v) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
a + 1 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
m4 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free m4 is Element of K27(VAR)
m4 <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
f is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (m4,f) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
variables_in m4 is non empty finite Element of K27(VAR)
p is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
5 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. a is Element of VAR
m4 / ((x. 0),(x. a)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in r is non empty finite Element of K27(VAR)
Free r is Element of K27(VAR)
r <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
f . (x. 0) is Element of M
f / ((x. a),(f . (x. 0))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (r,(f / ((x. a),(f . (x. 0))))) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
r2 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. r2 is Element of VAR
x. a is Element of VAR
p is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in p is non empty finite Element of K27(VAR)
Free p is Element of K27(VAR)
a is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
p <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (p,a) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
All ((x. 4),(x. a),p) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (All ((x. 4),(x. a),p)) is non empty finite Element of K27(VAR)
r is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. r is Element of VAR
p / ((x. a),(x. r)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r2 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in r2 is non empty finite Element of K27(VAR)
Free r2 is Element of K27(VAR)
r2 <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(r2 <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(r2 <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(r2 <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a . (x. a) is Element of M
a / ((x. r),(a . (x. a))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (r2,r) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
{(x. 4),(x. a)} is finite set
(variables_in p) \/ {(x. 4),(x. a)} is finite set
r . (x. r) is Element of M
r / ((x. a),(r . (x. r))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a / ((x. a),(r . (x. r))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(a / ((x. a),(r . (x. r)))) / ((x. r),(a . (x. a))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
{(x. a)} is finite set
(variables_in p) \ {(x. a)} is finite Element of K27(VAR)
{(x. r)} is finite set
r is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. r is Element of VAR
((variables_in p) \ {(x. a)}) \/ {(x. r)} is finite set
{(x. a)} is finite set
(Free p) \ {(x. a)} is Element of K27(VAR)
{(x. r)} is finite set
((Free p) \ {(x. a)}) \/ {(x. r)} is set
(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))))))) / ((x. a),(x. r)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))))) / ((x. a),(x. r)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),((Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))))) / ((x. a),(x. r)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))) / ((x. a),(x. r)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),((All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))) / ((x. a),(x. r)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),((All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))) / ((x. a),(x. r)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(p <=> ((x. 4) '=' (x. 0))) / ((x. a),(x. r)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),((p <=> ((x. 4) '=' (x. 0))) / ((x. a),(x. r)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),((p <=> ((x. 4) '=' (x. 0))) / ((x. a),(x. r)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),((p <=> ((x. 4) '=' (x. 0))) / ((x. a),(x. r)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
((x. 4) '=' (x. 0)) / ((x. a),(x. r)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r2 <=> (((x. 4) '=' (x. 0)) / ((x. a),(x. r))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(r2 <=> (((x. 4) '=' (x. 0)) / ((x. a),(x. r))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(r2 <=> (((x. 4) '=' (x. 0)) / ((x. a),(x. r))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(r2 <=> (((x. 4) '=' (x. 0)) / ((x. a),(x. r))))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a / ((x. a),(a . (x. a))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
{(x. 4)} is finite set
{(x. 0)} is finite set
{(x. 4),(x. 0)} is finite set
(variables_in p) \/ {(x. 4),(x. 0)} is finite set
((variables_in p) \/ {(x. 4),(x. 0)}) \/ {(x. 4)} is finite set
(((variables_in p) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)} is finite set
variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))))))) is non empty finite Element of K27(VAR)
variables_in (Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))))) is non empty finite Element of K27(VAR)
{(x. 3)} is finite set
(variables_in (Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) \/ {(x. 3)} is finite set
variables_in (All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))) is non empty finite Element of K27(VAR)
(variables_in (All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))) \/ {(x. 0)} is finite set
((variables_in (All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))) \/ {(x. 0)}) \/ {(x. 3)} is finite set
variables_in (p <=> ((x. 4) '=' (x. 0))) is non empty finite Element of K27(VAR)
(variables_in (p <=> ((x. 4) '=' (x. 0)))) \/ {(x. 4)} is finite set
((variables_in (p <=> ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)} is finite set
(((variables_in (p <=> ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} is finite set
variables_in ((x. 4) '=' (x. 0)) is non empty finite Element of K27(VAR)
(variables_in p) \/ (variables_in ((x. 4) '=' (x. 0))) is finite Element of K27(VAR)
((variables_in p) \/ (variables_in ((x. 4) '=' (x. 0)))) \/ {(x. 4)} is finite set
(((variables_in p) \/ (variables_in ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)} is finite set
((((variables_in p) \/ (variables_in ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} is finite set
((((variables_in p) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} is finite set
r is Element of M
r / ((x. 3),r) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 3),r)) . (x. r) is Element of M
a / ((x. 3),r) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
m4 is Element of M
(a / ((x. 3),r)) / ((x. 0),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((a / ((x. 3),r)) / ((x. 0),m4)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((a / ((x. 3),r)) / ((x. 0),m4)) / ((x. 4),m4)) . (x. 0) is Element of M
((a / ((x. 3),r)) / ((x. 0),m4)) . (x. 0) is Element of M
(((a / ((x. 3),r)) / ((x. 0),m4)) / ((x. 4),m4)) . (x. 4) is Element of M
(r / ((x. 3),r)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),r)) / ((x. 4),m4)) . (x. r) is Element of M
((r / ((x. 3),r)) / ((x. 4),m4)) / ((x. 0),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),r)) / ((x. 4),m4)) / ((x. 0),m4)) . (x. r) is Element of M
(a / ((x. 3),r)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((a / ((x. 3),r)) / ((x. 4),m4)) / ((x. 0),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((a / ((x. 3),r)) / ((x. 4),m4)) / ((x. 0),m4)) / ((x. r),(a . (x. a))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),r)) / ((x. 4),m4)) / ((x. 0),m4)) / ((x. a),(r . (x. r))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. a),(r . (x. r)))) / ((x. 3),r) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. a),(r . (x. r)))) / ((x. 3),r)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. a),(r . (x. r)))) / ((x. 3),r)) / ((x. 4),m4)) / ((x. 0),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(def_func' (r2,r)) . r is Element of M
(def_func' (p,a)) . r is Element of M
p is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in p is non empty finite Element of K27(VAR)
Free p is Element of K27(VAR)
a is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
p <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (p,a) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
r is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. r is Element of VAR
p is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in p is non empty finite Element of K27(VAR)
Free p is Element of K27(VAR)
a is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
p <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (p,a) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
r is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in r is non empty finite Element of K27(VAR)
Free r is Element of K27(VAR)
r2 is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (r,r2) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
r is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in r is non empty finite Element of K27(VAR)
Free r is Element of K27(VAR)
r is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (r,r) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free a is Element of K27(VAR)
a <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
m4 is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (a,m4) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
variables_in a is non empty finite Element of K27(VAR)
f is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. f is Element of VAR
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free H is Element of K27(VAR)
H <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
i is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (H,i) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
variables_in H is non empty finite Element of K27(VAR)
v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in a is non empty finite Element of K27(VAR)
Free a is Element of K27(VAR)
m4 is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (a,m4) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
(Free H) /\ (Free a) is Element of K27(VAR)
f is set
p is Element of VAR
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. a is Element of VAR
M is non empty set
H is Relation-like Function-like set
i is Relation-like Function-like set
i * H is Relation-like Function-like set
f is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free f is Element of K27(VAR)
f <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(f <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(f <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(f <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (f,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
p is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free p is Element of K27(VAR)
p <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (p,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
f '&' p is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 0),(x. 3),(x. 4),(f '&' p)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (All ((x. 0),(x. 3),(x. 4),(f '&' p))) is non empty finite Element of K27(VAR)
r2 is Element of VAR
variables_in (f '&' p) is non empty finite Element of K27(VAR)
{(x. 0),(x. 3),(x. 4)} is finite set
(variables_in (f '&' p)) \/ {(x. 0),(x. 3),(x. 4)} is finite set
f / ((x. 3),r2) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
p / ((x. 4),r2) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(f / ((x. 3),r2)) '&' (p / ((x. 4),r2)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex (r2,((f / ((x. 3),r2)) '&' (p / ((x. 4),r2)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free r is Element of K27(VAR)
r <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (r,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
r is set
Free ((f / ((x. 3),r2)) '&' (p / ((x. 4),r2))) is Element of K27(VAR)
{r2} is finite set
(Free ((f / ((x. 3),r2)) '&' (p / ((x. 4),r2)))) \ {r2} is Element of K27(VAR)
Free (f / ((x. 3),r2)) is Element of K27(VAR)
Free (p / ((x. 4),r2)) is Element of K27(VAR)
(Free (f / ((x. 3),r2))) \/ (Free (p / ((x. 4),r2))) is Element of K27(VAR)
{(x. 3)} is finite set
(Free f) \ {(x. 3)} is Element of K27(VAR)
((Free f) \ {(x. 3)}) \/ {r2} is set
{(x. 4)} is finite set
(Free p) \ {(x. 4)} is Element of K27(VAR)
((Free p) \ {(x. 4)}) \/ {r2} is set
variables_in f is non empty finite Element of K27(VAR)
variables_in p is non empty finite Element of K27(VAR)
(variables_in f) \/ (variables_in p) is finite Element of K27(VAR)
K28(VAR,M) is set
K27(K28(VAR,M)) is set
r is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
m4 is Element of M
r / ((x. 3),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
k is Element of M
(r / ((x. 3),m4)) / ((x. 0),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r / ((x. 3),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
H is Element of M
(r / ((x. 3),k)) / ((x. 0),H) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 3),m4)) / ((x. 0),H) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
v is Element of M
((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
v is Element of M
(((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,v)) . r2 is Element of M
((((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,v)) / ((x. 4),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 0),H)) / (r2,v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 0),H)) / (r2,v)) / ((x. 4),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 3),m4)) / ((x. 4),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 4),v)) / ((x. 0),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 4),v)) / ((x. 0),H) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 4),v)) / ((x. 0),H)) / ((x. 0),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) . (x. 0) is Element of M
((r / ((x. 3),m4)) / ((x. 0),H)) . (x. 0) is Element of M
((r / ((x. 3),k)) / ((x. 0),H)) / ((x. 4),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),k)) / ((x. 0),H)) / ((x. 4),v)) . (x. 0) is Element of M
((r / ((x. 3),k)) / ((x. 0),H)) . (x. 0) is Element of M
((((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,v)) / ((x. 3),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 0),k)) / ((x. 4),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 0),k)) / ((x. 4),v)) . (x. 0) is Element of M
((r / ((x. 3),m4)) / ((x. 0),k)) . (x. 0) is Element of M
(((r / ((x. 3),m4)) / ((x. 0),k)) / ((x. 4),v)) . (x. 4) is Element of M
(((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / ((x. 3),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / ((x. 3),k)) / (r2,v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r / ((x. 0),H) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 0),H)) / ((x. 4),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 0),H)) / ((x. 4),v)) / ((x. 3),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 0),H)) / ((x. 4),v)) / ((x. 3),k)) / (r2,v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),k)) / ((x. 0),H)) / ((x. 4),v)) / (r2,v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),k)) / ((x. 0),H)) / ((x. 4),v)) . (x. 4) is Element of M
(((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) . (x. 4) is Element of M
(((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 0),k)) / ((x. 4),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 0),k)) / ((x. 4),k)) . (x. 0) is Element of M
(((r / ((x. 3),k)) / ((x. 0),H)) / ((x. 4),v)) / (r2,k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 0),k)) / ((x. 4),k)) . (x. 4) is Element of M
(((r / ((x. 3),m4)) / ((x. 0),k)) / ((x. 4),k)) / ((x. 0),H) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 3),m4)) / ((x. 4),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 4),k)) / ((x. 0),H) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),k)) / (r2,k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,k)) . r2 is Element of M
((((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,k)) / ((x. 3),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / ((x. 3),k)) / (r2,k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 0),H)) / ((x. 4),v)) / ((x. 3),k)) / (r2,k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((((r / ((x. 3),m4)) / ((x. 0),H)) / ((x. 4),v)) / (r2,k)) / ((x. 4),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m4)) / ((x. 0),H)) / (r2,k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((r / ((x. 3),m4)) / ((x. 0),H)) / (r2,k)) / ((x. 4),k) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
K28(VAR,M) is set
K27(K28(VAR,M)) is set
r is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
a is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
a * r is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
r . (x. 3) is Element of M
(a * r) . (r . (x. 3)) is Element of M
r . (x. 4) is Element of M
m4 is Element of M
r / (r2,m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / (r2,m4)) . r2 is Element of M
(r / (r2,m4)) / ((x. 3),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / (r2,m4)) / ((x. 3),m4)) . (x. 3) is Element of M
a . (((r / (r2,m4)) / ((x. 3),m4)) . (x. 3)) is Element of M
((r / (r2,m4)) / ((x. 3),m4)) . (x. 4) is Element of M
(r / (r2,m4)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / (r2,m4)) / ((x. 4),m4)) . (x. 3) is Element of M
(r / (r2,m4)) . (x. 3) is Element of M
(r / (r2,m4)) . (x. 4) is Element of M
r . (((r / (r2,m4)) / ((x. 4),m4)) . (x. 3)) is Element of M
((r / (r2,m4)) / ((x. 4),m4)) . (x. 4) is Element of M
r . (r . (x. 3)) is Element of M
r / ((x. 4),(r . (r . (x. 3)))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 4),(r . (r . (x. 3))))) . (x. 4) is Element of M
r / (r2,(r . (r . (x. 3)))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / (r2,(r . (r . (x. 3))))) . r2 is Element of M
(r / (r2,(r . (r . (x. 3))))) / ((x. 4),(r . (r . (x. 3)))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 4),(r . (r . (x. 3))))) / (r2,(r . (r . (x. 3)))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 4),(r . (r . (x. 3))))) . (x. 3) is Element of M
r / ((x. 3),(r . (r . (x. 3)))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 3),(r . (r . (x. 3))))) . (x. 3) is Element of M
a . (r . (r . (x. 3))) is Element of M
(r / (r2,(r . (r . (x. 3))))) / ((x. 3),(r . (r . (x. 3)))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 3),(r . (r . (x. 3))))) / (r2,(r . (r . (x. 3)))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 3),(r . (r . (x. 3))))) . (x. 4) is Element of M
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free H is Element of K27(VAR)
H <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
i is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
v is Element of M
i / ((x. 3),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a is Element of M
(i / ((x. 3),v)) / ((x. 0),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
m4 is Element of M
(i / ((x. 3),v)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((i / ((x. 3),v)) / ((x. 4),m4)) / ((x. 0),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((i / ((x. 3),v)) / ((x. 0),a)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((i / ((x. 3),v)) / ((x. 0),a)) . (x. 0) is Element of M
(((i / ((x. 3),v)) / ((x. 0),a)) / ((x. 4),m4)) . (x. 0) is Element of M
(((i / ((x. 3),v)) / ((x. 0),a)) / ((x. 4),m4)) . (x. 4) is Element of M
(i / ((x. 3),v)) / ((x. 0),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((i / ((x. 3),v)) / ((x. 0),m4)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((i / ((x. 3),v)) / ((x. 0),m4)) / ((x. 4),m4)) . (x. 0) is Element of M
((i / ((x. 3),v)) / ((x. 0),m4)) . (x. 0) is Element of M
(((i / ((x. 3),v)) / ((x. 0),m4)) / ((x. 4),m4)) . (x. 4) is Element of M
((i / ((x. 3),v)) / ((x. 4),m4)) / ((x. 0),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
v is Element of M
i / ((x. 3),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a is Element of M
(i / ((x. 3),v)) / ((x. 0),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
m4 is Element of M
((i / ((x. 3),v)) / ((x. 0),a)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((i / ((x. 3),v)) / ((x. 0),a)) / ((x. 4),m4)) . (x. 0) is Element of M
((i / ((x. 3),v)) / ((x. 0),a)) . (x. 0) is Element of M
(((i / ((x. 3),v)) / ((x. 0),a)) / ((x. 4),m4)) . (x. 4) is Element of M
(i / ((x. 3),v)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((i / ((x. 3),v)) / ((x. 4),m4)) / ((x. 0),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
{(x. 3)} is finite set
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free H is Element of K27(VAR)
'not' H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
i is Relation-like Function-like set
v is Relation-like Function-like set
{(x. 3),(x. 3),(x. 4)} is finite set
{(x. 3)} \/ {(x. 3),(x. 4)} is finite set
a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free a is Element of K27(VAR)
a <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (a,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
m4 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free m4 is Element of K27(VAR)
m4 <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (m4,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
f is Relation-like Function-like set
dom f is set
rng f is set
the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a is set
r is set
f . r is set
r2 is Element of M
the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),r2) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
( the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),r2)) . (x. 3) is Element of M
f . r2 is set
(def_func (a,M)) . r2 is Element of M
(def_func (m4,M)) . r2 is Element of M
H '&' a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
('not' H) '&' m4 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(H '&' a) 'or' (('not' H) '&' m4) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free a is Element of K27(VAR)
a <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(a <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (a,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
Free ('not' H) is Element of K27(VAR)
Free (H '&' a) is Element of K27(VAR)
(Free H) \/ (Free a) is Element of K27(VAR)
Free (('not' H) '&' m4) is Element of K27(VAR)
(Free ('not' H)) \/ (Free m4) is Element of K27(VAR)
(Free (H '&' a)) \/ (Free (('not' H) '&' m4)) is Element of K27(VAR)
r is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r2 is Element of M
r / ((x. 3),r2) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r is Element of M
r is Element of M
m4 is Element of M
H is Element of M
(r / ((x. 3),r2)) / ((x. 4),H) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
k is Element of M
the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r2 is Element of M
(def_func (a,M)) . r2 is Element of M
def_func' (a, the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),r2) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
( the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),r2)) / ((x. 4),((def_func (a,M)) . r2)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (a, the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
def_func' (m4, the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
i . r2 is set
v . r2 is set
( the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),r2)) . (x. 3) is Element of M
p is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
p . r2 is Element of M
M is non empty set
H is Relation-like Function-like set
i is Relation-like Function-like set
H * i is Relation-like Function-like set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
x. 1 is Element of VAR
x. 2 is Element of VAR
{(x. 0),(x. 1),(x. 2)} is finite set
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free v is Element of K27(VAR)
a is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
v <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(v <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(v <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(v <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (v,a) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
m4 is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free m4 is Element of K27(VAR)
f is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
m4 <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(m4 <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (m4,f) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
variables_in m4 is non empty finite Element of K27(VAR)
r is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
5 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
r2 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
r is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in r is non empty finite Element of K27(VAR)
Free r is Element of K27(VAR)
r is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(r <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (r,r) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
r2 + 1 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
k is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. k is Element of VAR
r / ((x. 4),(x. k)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
m4 / ((x. 3),(x. k)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(r / ((x. 4),(x. k))) '&' (m4 / ((x. 3),(x. k))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. k),((r / ((x. 4),(x. k))) '&' (m4 / ((x. 3),(x. k))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free H is Element of K27(VAR)
H <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
a is set
v . a is set
m1 is Element of VAR
r . m1 is Element of M
f . m1 is Element of M
v is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (H,v) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
a is set
a is set
Free ((r / ((x. 4),(x. k))) '&' (m4 / ((x. 3),(x. k)))) is Element of K27(VAR)
{(x. k)} is finite set
(Free ((r / ((x. 4),(x. k))) '&' (m4 / ((x. 3),(x. k))))) \ {(x. k)} is Element of K27(VAR)
Free (r / ((x. 4),(x. k))) is Element of K27(VAR)
Free (m4 / ((x. 3),(x. k))) is Element of K27(VAR)
(Free (r / ((x. 4),(x. k)))) \/ (Free (m4 / ((x. 3),(x. k)))) is Element of K27(VAR)
{(x. 4)} is finite set
(Free r) \ {(x. 4)} is Element of K27(VAR)
((Free r) \ {(x. 4)}) \/ {(x. k)} is set
(Free m4) \ {(x. 3)} is Element of K27(VAR)
((Free m4) \ {(x. 3)}) \/ {(x. k)} is set
a is Element of VAR
m1 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. m1 is Element of VAR
variables_in (m4 / ((x. 3),(x. k))) is non empty finite Element of K27(VAR)
a is Element of M
r / ((x. 3),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
m1 is Element of M
m3 is Element of VAR
v / ((x. 3),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 3),a)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),a)) / ((x. k),m1)) . m3 is Element of M
(r / ((x. 3),a)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),a)) / ((x. k),m1)) . m3 is Element of M
(v / ((x. 3),a)) . m3 is Element of M
v . m3 is Element of M
r . m3 is Element of M
(r / ((x. 3),a)) . m3 is Element of M
f / ((x. 3),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
m3 is Element of M
(r / ((x. 3),a)) / ((x. 4),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),a)) / ((x. 4),m1)) . (x. 4) is Element of M
x is Element of M
(v / ((x. 3),a)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
n is Element of M
x is Element of VAR
v / ((x. 3),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 3),m1)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),m1)) / ((x. 4),x)) . x is Element of M
(v / ((x. 3),m1)) . x is Element of M
v . x is Element of M
f . x is Element of M
(f / ((x. 3),m1)) . x is Element of M
(f / ((x. 3),m1)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((f / ((x. 3),m1)) / ((x. 4),x)) . x is Element of M
x is Element of M
((v / ((x. 3),a)) / ((x. 4),x)) / ((x. k),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
x is Element of VAR
(v / ((x. 3),a)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),a)) / ((x. 4),x)) . (x. 4) is Element of M
(r / ((x. 3),a)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),a)) / ((x. 4),x)) . (x. 3) is Element of M
(r / ((x. 3),a)) . (x. 3) is Element of M
((v / ((x. 3),a)) / ((x. 4),x)) . (x. 3) is Element of M
(v / ((x. 3),a)) . (x. 3) is Element of M
((v / ((x. 3),a)) / ((x. 4),x)) . x is Element of M
((r / ((x. 3),a)) / ((x. 4),x)) . x is Element of M
(v / ((x. 3),a)) . x is Element of M
v . x is Element of M
(r / ((x. 3),a)) . x is Element of M
r . x is Element of M
(((v / ((x. 3),a)) / ((x. 4),x)) / ((x. k),x)) . (x. k) is Element of M
(((v / ((x. 3),a)) / ((x. 4),x)) / ((x. k),x)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 3),a)) / ((x. k),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),a)) / ((x. k),x)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),a)) / ((x. 4),x)) / ((x. k),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),a)) / ((x. 4),x)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((v / ((x. 3),a)) / ((x. 4),x)) / ((x. k),m1)) / ((x. 3),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
v / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 4),x)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 4),x)) / ((x. k),m1)) / ((x. 3),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),m1)) / ((x. 4),x)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(f / ((x. 3),m1)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(f / ((x. 3),m1)) . (x. 3) is Element of M
x is Element of VAR
v / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 4),x)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 4),x)) / ((x. k),m1)) . x is Element of M
f / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(f / ((x. 4),x)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((f / ((x. 4),x)) / ((x. k),m1)) . x is Element of M
(v / ((x. 4),x)) . x is Element of M
v . x is Element of M
f . x is Element of M
(f / ((x. 4),x)) . x is Element of M
variables_in (r / ((x. 4),(x. k))) is non empty finite Element of K27(VAR)
((r / ((x. 3),a)) / ((x. 4),m1)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),a)) / ((x. k),m1)) / ((x. 4),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),a)) / ((x. k),m1)) / ((x. 4),x) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),a)) / ((x. 4),x)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((f / ((x. 3),m1)) / ((x. 4),x)) . (x. 3) is Element of M
((f / ((x. 3),m1)) / ((x. 4),x)) / ((x. k),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((f / ((x. 4),x)) / ((x. k),m1)) / ((x. 3),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 4),x)) / ((x. k),m1)) / ((x. 3),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a is set
m1 is Element of M
(def_func' (H,v)) . m1 is Element of M
p is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
a is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
a * p is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
(a * p) . m1 is Element of M
p . m1 is Element of M
a . (p . m1) is Element of M
v / ((x. 3),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
n is Element of M
((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
x is Element of VAR
(v / ((x. 3),m1)) / ((x. 4),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 4) is Element of M
r / ((x. 3),m1) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(r / ((x. 3),m1)) / ((x. 4),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((r / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) is Element of M
(r / ((x. 3),m1)) . (x. 3) is Element of M
((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) is Element of M
(v / ((x. 3),m1)) . (x. 3) is Element of M
((v / ((x. 3),m1)) / ((x. 4),n)) . x is Element of M
((r / ((x. 3),m1)) / ((x. 4),n)) . x is Element of M
(v / ((x. 3),m1)) . x is Element of M
v . x is Element of M
(r / ((x. 3),m1)) . x is Element of M
r . x is Element of M
x is Element of VAR
v / ((x. 3),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x is Element of M
(v / ((x. 3),n)) . x is Element of M
v . x is Element of M
f . x is Element of M
f / ((x. 3),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(f / ((x. 3),n)) . x is Element of M
(f / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((f / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x is Element of M
(((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) . (x. k) is Element of M
(((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / ((x. 3),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
v / ((x. 4),((def_func' (H,v)) . m1)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / ((x. 3),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a . n is Element of M
(((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / ((x. 4),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 3),m1)) / ((x. k),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),m1)) / ((x. k),n)) / ((x. 4),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((v / ((x. 3),m1)) / ((x. 4),n)) / ((x. k),n) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(a * p) . a is set
(def_func' (H,v)) . a is set
x. 1 is Element of VAR
x. 2 is Element of VAR
{(x. 0),(x. 1),(x. 2)} is finite set
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free H is Element of K27(VAR)
H <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free i is Element of K27(VAR)
i <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(i <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(i <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(i <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free v is Element of K27(VAR)
'not' v is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (H,a) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
def_func' (i,a) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
m4 is Relation-like Function-like set
dom m4 is set
rng m4 is set
f is set
p is set
m4 . p is set
a is Element of M
a / ((x. 3),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(def_func' (H,a)) . a is Element of M
(def_func' (i,a)) . a is Element of M
v '&' H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
('not' v) '&' i is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(v '&' H) 'or' (('not' v) '&' i) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
p is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free p is Element of K27(VAR)
p <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (p,a) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
Free ('not' v) is Element of K27(VAR)
Free (('not' v) '&' i) is Element of K27(VAR)
(Free ('not' v)) \/ (Free i) is Element of K27(VAR)
a is set
Free (v '&' H) is Element of K27(VAR)
(Free (v '&' H)) \/ (Free (('not' v) '&' i)) is Element of K27(VAR)
(Free v) \/ (Free H) is Element of K27(VAR)
a is set
a is Element of M
a / ((x. 3),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r is Element of M
r2 is Element of M
r is Element of M
m4 is Element of M
(a / ((x. 3),a)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r is Element of M
a is Element of M
(def_func' (p,a)) . a is Element of M
a / ((x. 3),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(a / ((x. 3),a)) / ((x. 4),((def_func' (p,a)) . a)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(def_func' (H,a)) . a is Element of M
(def_func' (i,a)) . a is Element of M
f is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
f . a is Element of M
M is non empty set
id M is Relation-like M -defined M -valued Function-like one-to-one non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
(x. 3) '=' (x. 4) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
H is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free H is Element of K27(VAR)
H <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (H,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(VAR,M) is set
K27(K28(VAR,M)) is set
a is Element of M
v is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
v / ((x. 3),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(v / ((x. 3),a)) . (x. 3) is Element of M
(v / ((x. 3),a)) / ((x. 0),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
m4 is Element of M
((v / ((x. 3),a)) / ((x. 0),a)) / ((x. 4),m4) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(((v / ((x. 3),a)) / ((x. 0),a)) / ((x. 4),m4)) . (x. 0) is Element of M
((v / ((x. 3),a)) / ((x. 0),a)) . (x. 0) is Element of M
((v / ((x. 3),a)) / ((x. 0),a)) . (x. 3) is Element of M
(((v / ((x. 3),a)) / ((x. 0),a)) / ((x. 4),m4)) . (x. 3) is Element of M
(((v / ((x. 3),a)) / ((x. 0),a)) / ((x. 4),m4)) . (x. 4) is Element of M
the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a is Element of M
the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
( the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),a)) . (x. 3) is Element of M
( the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),a)) / ((x. 4),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(( the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),a)) / ((x. 4),a)) . (x. 4) is Element of M
(( the Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M)) / ((x. 3),a)) / ((x. 4),a)) . (x. 3) is Element of M
(def_func (H,M)) . a is Element of M
i is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
i . a is Element of M
M is non empty set
id M is Relation-like M -defined M -valued Function-like one-to-one non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set