Theorem cleljustALT 2185

Description: Alternate proof of cleljust 1998. It is kept here and should not be modified because it is referenced on the Metamath Proof Explorer Home Page (mmset.html) as an example of how DV conditions are inherited by substitutions. (Contributed by NM, 28-Jan-2004.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Distinct variable groups:   x, z   y, z

Proof of Theorem cleljustALT

Step	Hyp	Ref	Expression
1		ax-5 1839	. . 3 |- ( x e. y -> A. z x e. y )
2		elequ1 1997	. . 3 |- ( z = x -> ( z e. y <-> x e. y ) )
3	1, 2	equsexhv 2124	. 2 |- ( E. z ( z = x /\ z e. y ) <-> x e. y )
4	3	bicomi 214	1 |- ( x e. y <-> E. z ( z = x /\ z e. y ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by: (None)