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

Theorem zfpair 4689
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 4690. Instead, use zfpair2 4692 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

Proof of Theorem zfpair
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfpr2 4044 . 2
2 19.43 1693 . . . . 5
3 prlem2 963 . . . . . 6
43exbii 1667 . . . . 5
5 0ex 4582 . . . . . . . 8
65isseti 3115 . . . . . . 7
7 19.41v 1771 . . . . . . 7
86, 7mpbiran 918 . . . . . 6
9 p0ex 4639 . . . . . . . 8
109isseti 3115 . . . . . . 7
11 19.41v 1771 . . . . . . 7
1210, 11mpbiran 918 . . . . . 6
138, 12orbi12i 521 . . . . 5
142, 4, 133bitr3ri 276 . . . 4
1514abbii 2591 . . 3
16 dfpr2 4044 . . . . 5
17 pp0ex 4641 . . . . 5
1816, 17eqeltrri 2542 . . . 4
19 equequ2 1799 . . . . . . . 8
20 0inp0 4624 . . . . . . . 8
2119, 20prlem1 962 . . . . . . 7
2221alrimdv 1721 . . . . . 6
2322spimev 2010 . . . . 5
24 orcom 387 . . . . . . . 8
25 equequ2 1799 . . . . . . . . 9
2620con2i 120 . . . . . . . . 9
2725, 26prlem1 962 . . . . . . . 8
2824, 27syl7bi 230 . . . . . . 7
2928alrimdv 1721 . . . . . 6
3029spimev 2010 . . . . 5
3123, 30jaoi 379 . . . 4
3218, 31zfrep4 4571 . . 3
3315, 32eqeltri 2541 . 2
341, 33eqeltri 2541 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  {cab 2442   cvv 3109   c0 3784  {csn 4029  {cpr 4031
This theorem is referenced by:  axpr  4690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-pw 4014  df-sn 4030  df-pr 4032
  Copyright terms: Public domain W3C validator