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

Theorem zfpair 4184
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 4185. Instead, use zfpair2 4187 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 3630 . 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 4124 . . . . . . . 8  |-  (/)  e.  _V
65isseti 2769 . . . . . . 7  |-  E. z 
z  =  (/)
7 19.41v 2035 . . . . . . 7  |-  ( E. z ( z  =  (/)  /\  w  =  x )  <->  ( E. z 
z  =  (/)  /\  w  =  x ) )
86, 7mpbiran 889 . . . . . 6  |-  ( E. z ( z  =  (/)  /\  w  =  x )  <->  w  =  x
)
9 p0ex 4169 . . . . . . . 8  |-  { (/) }  e.  _V
109isseti 2769 . . . . . . 7  |-  E. z 
z  =  { (/) }
11 19.41v 2035 . . . . . . 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 2370 . . 3  |-  { w  |  ( w  =  x  \/  w  =  y ) }  =  { w  |  E. z ( ( z  =  (/)  \/  z  =  { (/) } )  /\  ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
) ) }
16 dfpr2 3630 . . . . 5  |-  { (/) ,  { (/) } }  =  { z  |  ( z  =  (/)  \/  z  =  { (/) } ) }
17 pp0ex 4171 . . . . 5  |-  { (/) ,  { (/) } }  e.  _V
1816, 17eqeltrri 2329 . . . 4  |-  { z  |  ( z  =  (/)  \/  z  =  { (/)
} ) }  e.  _V
19 equequ2 1830 . . . . . . . 8  |-  ( v  =  x  ->  (
w  =  v  <->  w  =  x ) )
20 0inp0 4154 . . . . . . . 8  |-  ( z  =  (/)  ->  -.  z  =  { (/) } )
2119, 20prlem1 933 . . . . . . 7  |-  ( v  =  x  ->  (
z  =  (/)  ->  (
( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
)  ->  w  =  v ) ) )
2221alrimdv 2015 . . . . . 6  |-  ( v  =  x  ->  (
z  =  (/)  ->  A. w
( ( ( z  =  (/)  /\  w  =  x )  \/  (
z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) ) )
2322a4imev 1998 . . . . 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 2015 . . . . . 6  |-  ( v  =  y  ->  (
z  =  { (/) }  ->  A. w ( ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y ) )  ->  w  =  v ) ) )
3029a4imev 1998 . . . . 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 4113 . . 3  |-  { w  |  E. z ( ( z  =  (/)  \/  z  =  { (/) } )  /\  ( ( z  =  (/)  /\  w  =  x )  \/  ( z  =  { (/) }  /\  w  =  y )
) ) }  e.  _V
3315, 32eqeltri 2328 . 2  |-  { w  |  ( w  =  x  \/  w  =  y ) }  e.  _V
341, 33eqeltri 2328 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 2244   _Vcvv 2763   (/)c0 3430   {csn 3614   {cpr 3615
This theorem is referenced by:  axpr  4185  isdrs2  14035  clatl  14182  dfdir2  24658  latdir  24662
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 1927  ax-ext 2239  ax-rep 4105  ax-sep 4115  ax-nul 4123  ax-pow 4160
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-pw 3601  df-sn 3620  df-pr 3621
  Copyright terms: Public domain W3C validator