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

Metamath Proof Explorer

Theorem zfpair2

Description: Derive the abbreviated version of the Axiom of Pairing from ax-pr . See zfpair for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006)

Ref Expression
Assertion zfpair2 
|- { x , y } e. _V

Proof

Step Hyp Ref Expression
1 ax-pr 
 |-  E. z A. w ( ( w = x \/ w = y ) -> w e. z )
2 1 sepexi 
 |-  E. z A. w ( w e. z <-> ( w = x \/ w = 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 6 albii 
 |-  ( A. w ( w e. z <-> w e. { x , y } ) <-> A. w ( w e. z <-> ( w = x \/ w = y ) ) )
8 3 7 bitri 
 |-  ( z = { x , y } <-> A. w ( w e. z <-> ( w = x \/ w = y ) ) )
9 8 exbii 
 |-  ( E. z z = { x , y } <-> E. z A. w ( w e. z <-> ( w = x \/ w = y ) ) )
10 2 9 mpbir 
 |-  E. z z = { x , y }
11 10 issetri 
 |-  { x , y } e. _V