MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zfpair Unicode version

Theorem zfpair 4361
Description: The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of [TakeutiZaring] p. 15. In some textbooks this is stated as a separate axiom; here we show it is redundant since it can be derived from the other axioms.

This theorem should not be referenced by any proof other than axpr 4362. Instead, use zfpair2 4364 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)

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

Proof of Theorem zfpair
Dummy variables  z  w  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfpr2 3790 . 2  |-  { x ,  y }  =  { w  |  (
w  =  x  \/  w  =  y ) }
2 19.43 1612 . . . . 5  |-  ( E. z ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  <->  ( E. z ( z  =  (/)  /\  w  =  x )  \/  E. z
( z  =  { (/)
}  /\  w  =  y ) ) )
3 prlem2 930 . . . . . 6  |-  ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) )  <-> 
( ( z  =  (/)  \/  z  =  { (/)
} )  /\  (
( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) ) ) )
43exbii 1589 . . . . 5  |-  ( E. z ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  <->  E. z
( ( z  =  (/)  \/  z  =  { (/)
} )  /\  (
( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) ) ) )
5 0ex 4299 . . . . . . . 8  |-  (/)  e.  _V
65isseti 2922 . . . . . . 7  |-  E. z 
z  =  (/)
7 19.41v 1920 . . . . . . 7  |-  ( E. z ( z  =  (/)  /\  w  =  x )  <->  ( E. z 
z  =  (/)  /\  w  =  x ) )
86, 7mpbiran 885 . . . . . 6  |-  ( E. z ( z  =  (/)  /\  w  =  x )  <->  w  =  x
)
9 p0ex 4346 . . . . . . . 8  |-  { (/) }  e.  _V
109isseti 2922 . . . . . . 7  |-  E. z 
z  =  { (/) }
11 19.41v 1920 . . . . . . 7  |-  ( E. z ( z  =  { (/) }  /\  w  =  y )  <->  ( E. z  z  =  { (/)
}  /\  w  =  y ) )
1210, 11mpbiran 885 . . . . . 6  |-  ( E. z ( z  =  { (/) }  /\  w  =  y )  <->  w  =  y )
138, 12orbi12i 508 . . . . 5  |-  ( ( E. z ( z  =  (/)  /\  w  =  x )  \/  E. z ( z  =  { (/) }  /\  w  =  y ) )  <-> 
( w  =  x  \/  w  =  y ) )
142, 4, 133bitr3ri 268 . . . 4  |-  ( ( w  =  x  \/  w  =  y )  <->  E. z ( ( z  =  (/)  \/  z  =  { (/) } )  /\  ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
) ) )
1514abbii 2516 . . 3  |-  { w  |  ( w  =  x  \/  w  =  y ) }  =  { w  |  E. z ( ( z  =  (/)  \/  z  =  { (/) } )  /\  ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
) ) }
16 dfpr2 3790 . . . . 5  |-  { (/) ,  { (/) } }  =  { z  |  ( z  =  (/)  \/  z  =  { (/) } ) }
17 pp0ex 4348 . . . . 5  |-  { (/) ,  { (/) } }  e.  _V
1816, 17eqeltrri 2475 . . . 4  |-  { z  |  ( z  =  (/)  \/  z  =  { (/)
} ) }  e.  _V
19 equequ2 1694 . . . . . . . 8  |-  ( v  =  x  ->  (
w  =  v  <->  w  =  x ) )
20 0inp0 4331 . . . . . . . 8  |-  ( z  =  (/)  ->  -.  z  =  { (/) } )
2119, 20prlem1 929 . . . . . . 7  |-  ( v  =  x  ->  (
z  =  (/)  ->  (
( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
)  ->  w  =  v ) ) )
2221alrimdv 1640 . . . . . 6  |-  ( v  =  x  ->  (
z  =  (/)  ->  A. w
( ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) ) )
2322spimev 1962 . . . . 5  |-  ( z  =  (/)  ->  E. v A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) )
24 orcom 377 . . . . . . . 8  |-  ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) )  <-> 
( ( z  =  { (/) }  /\  w  =  y )  \/  ( z  =  (/)  /\  w  =  x ) ) )
25 equequ2 1694 . . . . . . . . 9  |-  ( v  =  y  ->  (
w  =  v  <->  w  =  y ) )
2620con2i 114 . . . . . . . . 9  |-  ( z  =  { (/) }  ->  -.  z  =  (/) )
2725, 26prlem1 929 . . . . . . . 8  |-  ( v  =  y  ->  (
z  =  { (/) }  ->  ( ( ( z  =  { (/) }  /\  w  =  y )  \/  ( z  =  (/)  /\  w  =  x ) )  ->  w  =  v )
) )
2824, 27syl7bi 222 . . . . . . 7  |-  ( v  =  y  ->  (
z  =  { (/) }  ->  ( ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) ) )
2928alrimdv 1640 . . . . . 6  |-  ( v  =  y  ->  (
z  =  { (/) }  ->  A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) ) )
3029spimev 1962 . . . . 5  |-  ( z  =  { (/) }  ->  E. v A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
)  ->  w  =  v ) )
3123, 30jaoi 369 . . . 4  |-  ( ( z  =  (/)  \/  z  =  { (/) } )  ->  E. v A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
)  ->  w  =  v ) )
3218, 31zfrep4 4288 . . 3  |-  { w  |  E. z ( ( z  =  (/)  \/  z  =  { (/) } )  /\  ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
) ) }  e.  _V
3315, 32eqeltri 2474 . 2  |-  { w  |  ( w  =  x  \/  w  =  y ) }  e.  _V
341, 33eqeltri 2474 1  |-  { x ,  y }  e.  _V
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    /\ wa 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1721   {cab 2390   _Vcvv 2916   (/)c0 3588   {csn 3774   {cpr 3775
This theorem is referenced by:  axpr  4362  clatl  14498
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-pw 3761  df-sn 3780  df-pr 3781
  Copyright terms: Public domain W3C validator