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

Theorem zfpair 4103
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 4104. Instead, use zfpair2 4106 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
StepHypRef Expression
1 dfpr2 3557 . 2  |-  { x ,  y }  =  { w  |  (
w  =  x  \/  w  =  y ) }
2 19.43 1604 . . . . 5  |-  ( E. z ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  <->  ( E. z ( z  =  (/)  /\  w  =  x )  \/  E. z
( z  =  { (/)
}  /\  w  =  y ) ) )
3 prlem2 934 . . . . . 6  |-  ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) )  <-> 
( ( z  =  (/)  \/  z  =  { (/)
} )  /\  (
( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) ) ) )
43exbii 1580 . . . . 5  |-  ( E. z ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  <->  E. z
( ( z  =  (/)  \/  z  =  { (/)
} )  /\  (
( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) ) ) )
5 0ex 4044 . . . . . . . 8  |-  (/)  e.  _V
65isseti 2731 . . . . . . 7  |-  E. z 
z  =  (/)
7 19.41v 2034 . . . . . . 7  |-  ( E. z ( z  =  (/)  /\  w  =  x )  <->  ( E. z 
z  =  (/)  /\  w  =  x ) )
86, 7mpbiran 889 . . . . . 6  |-  ( E. z ( z  =  (/)  /\  w  =  x )  <->  w  =  x
)
9 p0ex 4088 . . . . . . . 8  |-  { (/) }  e.  _V
109isseti 2731 . . . . . . 7  |-  E. z 
z  =  { (/) }
11 19.41v 2034 . . . . . . 7  |-  ( E. z ( z  =  { (/) }  /\  w  =  y )  <->  ( E. z  z  =  { (/)
}  /\  w  =  y ) )
1210, 11mpbiran 889 . . . . . 6  |-  ( E. z ( z  =  { (/) }  /\  w  =  y )  <->  w  =  y )
138, 12orbi12i 509 . . . . 5  |-  ( ( E. z ( z  =  (/)  /\  w  =  x )  \/  E. z ( z  =  { (/) }  /\  w  =  y ) )  <-> 
( w  =  x  \/  w  =  y ) )
142, 4, 133bitr3ri 269 . . . 4  |-  ( ( w  =  x  \/  w  =  y )  <->  E. z ( ( z  =  (/)  \/  z  =  { (/) } )  /\  ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
) ) )
1514abbii 2361 . . 3  |-  { w  |  ( w  =  x  \/  w  =  y ) }  =  { w  |  E. z ( ( z  =  (/)  \/  z  =  { (/) } )  /\  ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
) ) }
16 dfpr2 3557 . . . . 5  |-  { (/) ,  { (/) } }  =  { z  |  ( z  =  (/)  \/  z  =  { (/) } ) }
17 pp0ex 4090 . . . . 5  |-  { (/) ,  { (/) } }  e.  _V
1816, 17eqeltrri 2324 . . . 4  |-  { z  |  ( z  =  (/)  \/  z  =  { (/)
} ) }  e.  _V
19 equequ2 1830 . . . . . . . 8  |-  ( v  =  x  ->  (
w  =  v  <->  w  =  x ) )
20 0inp0 4073 . . . . . . . 8  |-  ( z  =  (/)  ->  -.  z  =  { (/) } )
2119, 20prlem1 933 . . . . . . 7  |-  ( v  =  x  ->  (
z  =  (/)  ->  (
( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
)  ->  w  =  v ) ) )
2221alrimdv 2014 . . . . . 6  |-  ( v  =  x  ->  (
z  =  (/)  ->  A. w
( ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) ) )
2322a4imev 1997 . . . . 5  |-  ( z  =  (/)  ->  E. v A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) )
24 orcom 378 . . . . . . . 8  |-  ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) )  <-> 
( ( z  =  { (/) }  /\  w  =  y )  \/  ( z  =  (/)  /\  w  =  x ) ) )
25 equequ2 1830 . . . . . . . . 9  |-  ( v  =  y  ->  (
w  =  v  <->  w  =  y ) )
2620con2i 114 . . . . . . . . 9  |-  ( z  =  { (/) }  ->  -.  z  =  (/) )
2725, 26prlem1 933 . . . . . . . 8  |-  ( v  =  y  ->  (
z  =  { (/) }  ->  ( ( ( z  =  { (/) }  /\  w  =  y )  \/  ( z  =  (/)  /\  w  =  x ) )  ->  w  =  v )
) )
2824, 27syl7bi 223 . . . . . . 7  |-  ( v  =  y  ->  (
z  =  { (/) }  ->  ( ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) ) )
2928alrimdv 2014 . . . . . 6  |-  ( v  =  y  ->  (
z  =  { (/) }  ->  A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) ) )
3029a4imev 1997 . . . . 5  |-  ( z  =  { (/) }  ->  E. v A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
)  ->  w  =  v ) )
3123, 30jaoi 370 . . . 4  |-  ( ( z  =  (/)  \/  z  =  { (/) } )  ->  E. v A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
)  ->  w  =  v ) )
3218, 31zfrep4 4033 . . 3  |-  { w  |  E. z ( ( z  =  (/)  \/  z  =  { (/) } )  /\  ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
) ) }  e.  _V
3315, 32eqeltri 2323 . 2  |-  { w  |  ( w  =  x  \/  w  =  y ) }  e.  _V
341, 33eqeltri 2323 1  |-  { x ,  y }  e.  _V
Colors of variables: wff set class
Syntax hints:    -> wi 6    \/ wo 359    /\ wa 360   A.wal 1532   E.wex 1537    = wceq 1619    e. wcel 1621   {cab 2239   _Vcvv 2725   (/)c0 3359   {csn 3541   {cpr 3542
This theorem is referenced by:  axpr  4104  isdrs2  13879  clatl  14026  dfdir2  24386  latdir  24390
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-rep 4025  ax-sep 4035  ax-nul 4043  ax-pow 4079
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2727  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-pw 3529  df-sn 3547  df-pr 3548
  Copyright terms: Public domain W3C validator