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

Theorem zfpair 4730
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 4731. Instead, use zfpair2 4733 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 {𝑥, 𝑦} ∈ V

Proof of Theorem zfpair
Dummy variables 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfpr2 4046 . 2 {𝑥, 𝑦} = {𝑤 ∣ (𝑤 = 𝑥𝑤 = 𝑦)}
2 19.43 1780 . . . . 5 (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)))
3 prlem2 997 . . . . . 6 (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
43exbii 1752 . . . . 5 (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
5 0ex 4617 . . . . . . . 8 ∅ ∈ V
65isseti 3086 . . . . . . 7 𝑧 𝑧 = ∅
7 19.41v 1864 . . . . . . 7 (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ (∃𝑧 𝑧 = ∅ ∧ 𝑤 = 𝑥))
86, 7mpbiran 954 . . . . . 6 (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ 𝑤 = 𝑥)
9 p0ex 4678 . . . . . . . 8 {∅} ∈ V
109isseti 3086 . . . . . . 7 𝑧 𝑧 = {∅}
11 19.41v 1864 . . . . . . 7 (∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦) ↔ (∃𝑧 𝑧 = {∅} ∧ 𝑤 = 𝑦))
1210, 11mpbiran 954 . . . . . 6 (∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦) ↔ 𝑤 = 𝑦)
138, 12orbi12i 541 . . . . 5 ((∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (𝑤 = 𝑥𝑤 = 𝑦))
142, 4, 133bitr3ri 289 . . . 4 ((𝑤 = 𝑥𝑤 = 𝑦) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
1514abbii 2630 . . 3 {𝑤 ∣ (𝑤 = 𝑥𝑤 = 𝑦)} = {𝑤 ∣ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)))}
16 dfpr2 4046 . . . . 5 {∅, {∅}} = {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})}
17 pp0ex 4680 . . . . 5 {∅, {∅}} ∈ V
1816, 17eqeltrri 2589 . . . 4 {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})} ∈ V
19 equequ2 1903 . . . . . . . 8 (𝑣 = 𝑥 → (𝑤 = 𝑣𝑤 = 𝑥))
20 0inp0 4662 . . . . . . . 8 (𝑧 = ∅ → ¬ 𝑧 = {∅})
2119, 20prlem1 996 . . . . . . 7 (𝑣 = 𝑥 → (𝑧 = ∅ → (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
2221alrimdv 1810 . . . . . 6 (𝑣 = 𝑥 → (𝑧 = ∅ → ∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
2322spimev 2150 . . . . 5 (𝑧 = ∅ → ∃𝑣𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
24 orcom 400 . . . . . . . 8 (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = {∅} ∧ 𝑤 = 𝑦) ∨ (𝑧 = ∅ ∧ 𝑤 = 𝑥)))
25 equequ2 1903 . . . . . . . . 9 (𝑣 = 𝑦 → (𝑤 = 𝑣𝑤 = 𝑦))
2620con2i 132 . . . . . . . . 9 (𝑧 = {∅} → ¬ 𝑧 = ∅)
2725, 26prlem1 996 . . . . . . . 8 (𝑣 = 𝑦 → (𝑧 = {∅} → (((𝑧 = {∅} ∧ 𝑤 = 𝑦) ∨ (𝑧 = ∅ ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑣)))
2824, 27syl7bi 243 . . . . . . 7 (𝑣 = 𝑦 → (𝑧 = {∅} → (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
2928alrimdv 1810 . . . . . 6 (𝑣 = 𝑦 → (𝑧 = {∅} → ∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
3029spimev 2150 . . . . 5 (𝑧 = {∅} → ∃𝑣𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
3123, 30jaoi 392 . . . 4 ((𝑧 = ∅ ∨ 𝑧 = {∅}) → ∃𝑣𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
3218, 31zfrep4 4605 . . 3 {𝑤 ∣ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)))} ∈ V
3315, 32eqeltri 2588 . 2 {𝑤 ∣ (𝑤 = 𝑥𝑤 = 𝑦)} ∈ V
341, 33eqeltri 2588 1 {𝑥, 𝑦} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381  wa 382  wal 1472   = wceq 1474  wex 1694  wcel 1938  {cab 2500  Vcvv 3077  c0 3777  {csn 4028  {cpr 4030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-pw 4013  df-sn 4029  df-pr 4031
This theorem is referenced by:  axpr  4731
  Copyright terms: Public domain W3C validator