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

Theorem zfpair 4934
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 4935. Instead, use zfpair2 4937 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 4228 . 2 {𝑥, 𝑦} = {𝑤 ∣ (𝑤 = 𝑥𝑤 = 𝑦)}
2 19.43 1850 . . . . 5 (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)))
3 prlem2 1026 . . . . . 6 (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
43exbii 1814 . . . . 5 (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
5 0ex 4823 . . . . . . . 8 ∅ ∈ V
65isseti 3240 . . . . . . 7 𝑧 𝑧 = ∅
7 19.41v 1917 . . . . . . 7 (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ (∃𝑧 𝑧 = ∅ ∧ 𝑤 = 𝑥))
86, 7mpbiran 973 . . . . . 6 (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ 𝑤 = 𝑥)
9 p0ex 4883 . . . . . . . 8 {∅} ∈ V
109isseti 3240 . . . . . . 7 𝑧 𝑧 = {∅}
11 19.41v 1917 . . . . . . 7 (∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦) ↔ (∃𝑧 𝑧 = {∅} ∧ 𝑤 = 𝑦))
1210, 11mpbiran 973 . . . . . 6 (∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦) ↔ 𝑤 = 𝑦)
138, 12orbi12i 542 . . . . 5 ((∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (𝑤 = 𝑥𝑤 = 𝑦))
142, 4, 133bitr3ri 291 . . . 4 ((𝑤 = 𝑥𝑤 = 𝑦) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
1514abbii 2768 . . 3 {𝑤 ∣ (𝑤 = 𝑥𝑤 = 𝑦)} = {𝑤 ∣ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)))}
16 dfpr2 4228 . . . . 5 {∅, {∅}} = {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})}
17 pp0ex 4885 . . . . 5 {∅, {∅}} ∈ V
1816, 17eqeltrri 2727 . . . 4 {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})} ∈ V
19 equequ2 1999 . . . . . . . 8 (𝑣 = 𝑥 → (𝑤 = 𝑣𝑤 = 𝑥))
20 0inp0 4867 . . . . . . . 8 (𝑧 = ∅ → ¬ 𝑧 = {∅})
2119, 20prlem1 1025 . . . . . . 7 (𝑣 = 𝑥 → (𝑧 = ∅ → (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
2221alrimdv 1897 . . . . . 6 (𝑣 = 𝑥 → (𝑧 = ∅ → ∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
2322spimev 2295 . . . . 5 (𝑧 = ∅ → ∃𝑣𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
24 orcom 401 . . . . . . . 8 (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = {∅} ∧ 𝑤 = 𝑦) ∨ (𝑧 = ∅ ∧ 𝑤 = 𝑥)))
25 equequ2 1999 . . . . . . . . 9 (𝑣 = 𝑦 → (𝑤 = 𝑣𝑤 = 𝑦))
2620con2i 134 . . . . . . . . 9 (𝑧 = {∅} → ¬ 𝑧 = ∅)
2725, 26prlem1 1025 . . . . . . . 8 (𝑣 = 𝑦 → (𝑧 = {∅} → (((𝑧 = {∅} ∧ 𝑤 = 𝑦) ∨ (𝑧 = ∅ ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑣)))
2824, 27syl7bi 245 . . . . . . 7 (𝑣 = 𝑦 → (𝑧 = {∅} → (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
2928alrimdv 1897 . . . . . 6 (𝑣 = 𝑦 → (𝑧 = {∅} → ∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
3029spimev 2295 . . . . 5 (𝑧 = {∅} → ∃𝑣𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
3123, 30jaoi 393 . . . 4 ((𝑧 = ∅ ∨ 𝑧 = {∅}) → ∃𝑣𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
3218, 31zfrep4 4812 . . 3 {𝑤 ∣ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)))} ∈ V
3315, 32eqeltri 2726 . 2 {𝑤 ∣ (𝑤 = 𝑥𝑤 = 𝑦)} ∈ V
341, 33eqeltri 2726 1 {𝑥, 𝑦} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383  wal 1521   = wceq 1523  wex 1744  wcel 2030  {cab 2637  Vcvv 3231  c0 3948  {csn 4210  {cpr 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-pw 4193  df-sn 4211  df-pr 4213
This theorem is referenced by:  axpr  4935
  Copyright terms: Public domain W3C validator