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

Metamath Proof Explorer

Theorem axprALT

Description: Alternate proof of axpr . (Contributed by NM, 14-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion axprALT 
|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )

Proof

Step Hyp Ref Expression
1 zfpair 
 |-  { x , y } e. _V
2 1 isseti 
 |-  E. z z = { x , y }
3 dfcleq 
 |-  ( z = { x , y } <-> A. w ( w e. z <-> w e. { x , y } ) )
4 vex 
 |-  w e. _V
5 4 elpr 
 |-  ( w e. { x , y } <-> ( w = x \/ w = y ) )
6 5 bibi2i 
 |-  ( ( w e. z <-> w e. { x , y } ) <-> ( w e. z <-> ( w = x \/ w = y ) ) )
7 biimpr 
 |-  ( ( w e. z <-> ( w = x \/ w = y ) ) -> ( ( w = x \/ w = y ) -> w e. z ) )
8 6 7 sylbi 
 |-  ( ( w e. z <-> w e. { x , y } ) -> ( ( w = x \/ w = y ) -> w e. z ) )
9 8 alimi 
 |-  ( A. w ( w e. z <-> w e. { x , y } ) -> A. w ( ( w = x \/ w = y ) -> w e. z ) )
10 3 9 sylbi 
 |-  ( z = { x , y } -> A. w ( ( w = x \/ w = y ) -> w e. z ) )
11 2 10 eximii 
 |-  E. z A. w ( ( w = x \/ w = y ) -> w e. z )