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

Metamath Proof Explorer

Theorem elALT

Description: Alternate proof of el , shorter but requiring ax-sep . (Contributed by NM, 4-Jan-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elALT 
|- E. y x e. y

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 selsALT 
 |-  ( x e. _V -> E. y x e. y )
3 1 2 ax-mp 
 |-  E. y x e. y