Theorem cleljust 2163

Description: When the class variables in definition df-clel 2424 are replaced with setvar 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 setvar variables in wel 1871 with the class variables in wcel 1870. 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-5 1751	. . 3 |- ( x e. y -> A. z x e. y )
2		elequ1 1873	. . 3 |- ( z = x -> ( z e. y <-> x e. y ) )
3	1, 2	equsexh 2095	. 2 |- ( E. z ( z = x /\ z e. y ) <-> x e. y )
4	3	bicomi 205	1 |- ( x e. y <-> E. z ( z = x /\ z e. y ) )

Syntax hints:   <-> wb 187   /\ wa 370   E.wex 1659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-10 1889  ax-12 1907  ax-13 2055

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664

This theorem is referenced by: (None)