Theorem axpr 2773

Description: Unabbreviated version of the Axiom of Pairing of ZF set theory, derived as a theorem from the other axioms.

This theorem should not be referenced by any proof. Instead, use ax-pr 2774 below so that the uses of the Axiom of Pairing can be more easily identified.

Assertion

Ref	Expression
axpr	⊢ ∃z∀w((w = x ⋁ w = y) → w ∈ z)

Distinct variable groups:   x,z,w   y,z,w

Proof of Theorem axpr

Step	Hyp	Ref	Expression
1		zfpair 2772	. . 3 ⊢ {x, y} ∈ V
2	1	isseti 1811	. 2 ⊢ ∃z z = {x, y}
3		dfcleq 1468	. . . 4 ⊢ (z = {x, y} ↔ ∀w(w ∈ z ↔ w ∈ {x, y}))
4		visset 1809	. . . . . . . 8 ⊢ w ∈ V
5	4	elpr 2420	. . . . . . 7 ⊢ (w ∈ {x, y} ↔ (w = x ⋁ w = y))
6	5	bibi2i 607	. . . . . 6 ⊢ ((w ∈ z ↔ w ∈ {x, y}) ↔ (w ∈ z ↔ (w = x ⋁ w = y)))
7		bi2 149	. . . . . 6 ⊢ ((w ∈ z ↔ (w = x ⋁ w = y)) → ((w = x ⋁ w = y) → w ∈ z))
8	6, 7	sylbi 199	. . . . 5 ⊢ ((w ∈ z ↔ w ∈ {x, y}) → ((w = x ⋁ w = y) → w ∈ z))
9	8	19.20i 990	. . . 4 ⊢ (∀w(w ∈ z ↔ w ∈ {x, y}) → ∀w((w = x ⋁ w = y) → w ∈ z))
10	3, 9	sylbi 199	. . 3 ⊢ (z = {x, y} → ∀w((w = x ⋁ w = y) → w ∈ z))
11	10	19.22i 1038	. 2 ⊢ (∃z z = {x, y} → ∃z∀w((w = x ⋁ w = y) → w ∈ z))
12	2, 11	ax-mp 7	1 ⊢ ∃z∀w((w = x ⋁ w = y) → w ∈ z)

Syntax hints:   → wi 3   ↔ wb 146   ⋁ wo 222  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  {cpr 2406

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409

Copyright terms: Public domain