Theorem zfpair2 5396

Description: Derive the abbreviated version of the Axiom of Pairing from ax-pr 5395. See zfpair 5387 for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006.)

Assertion

Ref	Expression
zfpair2	⊢ {𝑥, 𝑦} ∈ V

Proof of Theorem zfpair2

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-pr 5395	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
2	1	sepexi 5259	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦))
3		dfcleq 2756	. . . . 5 ⊢ (𝑧 = {𝑥, 𝑦} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝑥, 𝑦}))
4		vex 3458	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4609	. . . . . . 7 ⊢ (𝑤 ∈ {𝑥, 𝑦} ↔ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦))
6	5	bibi2i 340	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝑥, 𝑦}) ↔ (𝑤 ∈ 𝑧 ↔ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)))
7	6	albii 1852	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝑥, 𝑦}) ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)))
8	3, 7	bitri 278	. . . 4 ⊢ (𝑧 = {𝑥, 𝑦} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)))
9	8	exbii 1881	. . 3 ⊢ (∃𝑧 𝑧 = {𝑥, 𝑦} ↔ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)))
10	2, 9	mpbir 234	. 2 ⊢ ∃𝑧 𝑧 = {𝑥, 𝑦}
11	10	issetri 3473	1 ⊢ {𝑥, 𝑦} ∈ V

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147  Vcvv 3454  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  vsnex  5397  prexOLD  5405  pwssun  5547  xpsspw  5792  funopg  6594  fiint  9346  brdom7disj  10637  brdom6disj  10638  2pthfrgrrn  30913  sprval  48766  prprval  48801  reupr  48809