Theorem cleljust 1323

Description: When the class variables in definition df-clel 1465 are replaced with set variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the set variables in wel 956 with the class variables in wcel 955.

Assertion

Ref	Expression
cleljust	|- (x e. y <-> E.z(z = x /\ z e. y))

Distinct variable groups:   x,z   y,z

Proof of Theorem cleljust

Step	Hyp	Ref	Expression
1		ax-17 968	. . 3 |- (x e. y -> A.z x e. y)
2		elequ1 1132	. . 3 |- (z = x -> (z e. y <-> x e. y))
3	1, 2	equsex 1148	. 2 |- (E.z(z = x /\ z e. y) <-> x e. y)
4	3	bicomi 172	1 |- (x e. y <-> E.z(z = x /\ z e. y))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-8 961  ax-12 965  ax-13 966  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain