Theorem cleljust 2064

Description: When the class variables in definition df-clel 2400 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 1722 with the class variables in wcel 1721. Note: This proof is referenced on the Metamath Proof Explorer Home Page and shouldn't be changed. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.)

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 1623	. . 3 |- ( x e. y -> A. z x e. y )
2		elequ1 1724	. . 3 |- ( z = x -> ( z e. y <-> x e. y ) )
3	1, 2	equsexh 1971	. 2 |- ( E. z ( z = x /\ z e. y ) <-> x e. y )
4	3	bicomi 194	1 |- ( x e. y <-> E. z ( z = x /\ z e. y ) )

Syntax hints:   <-> wb 177   /\ wa 359   E.wex 1547

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-6 1740  ax-11 1757  ax-12 1946

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551