This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cleljustALT2

Description: Alternate proof of cleljust . Compared with cleljustALT , it uses nfv followed by equsexv instead of ax-5 followed by equsexhv , so it uses the idiom F/ x ph instead of ph -> A. x ph to express nonfreeness. This style is generally preferred for later theorems. (Contributed by NM, 28-Jan-2004) (Revised by Mario Carneiro, 21-Dec-2016) (Revised by BJ, 29-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ z x e. y
2 elequ1 
 |-  ( z = x -> ( z e. y <-> x e. y ) )
3 1 2 equsexv 
 |-  ( E. z ( z = x /\ z e. y ) <-> x e. y )
4 3 bicomi 
 |-  ( x e. y <-> E. z ( z = x /\ z e. y ) )