Theorem prexg 4347

Description: The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3821, prprc1 3819, and prprc2 3820. (Contributed by Jim Kingdon, 16-Sep-2018.)

Assertion

Ref	Expression
prexg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)

Proof of Theorem prexg

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		preq2 3788	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2307	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 4345	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 2883	. . . 4 ⊢ (𝐵 ∈ 𝑊 → {𝑥, 𝐵} ∈ V)
5		preq1 3787	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2307	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 154	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ 𝑊 → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 2896	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → {𝐴, 𝐵} ∈ V))
9	8	imp 124	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  Vcvv 2821  {cpr 3709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pr 4344

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3714  df-pr 3715

This theorem is referenced by:  prelpw  4351  prelpwi  4352  opexg  4366  opi2  4371  opth  4375  opeqsn  4391  opeqpr  4392  uniop  4394  unex  4585  tpexg  4588  op1stb  4622  op1stbg  4623  onun2  4635  opthreg  4701  relop  4928  acexmidlemv  6077  2oex  6698  en2prd  7100  pw2f1odclem  7128  pr2ne  7532  exmidonfinlem  7539  exmidaclem  7558  sup3exmid  9281  xrex  10241  2strbasg  13457  2stropg  13458  xpsfval  13652  prdsex  14155  prdsval  14156  xpsval  14184  struct2slots2dom  16262  structiedg0val  16264  edgstruct  16288  umgrbien  16334  upgr1edc  16345  upgr1eopdc  16347  uspgr1edc  16464  usgr1e  16465  uspgr1eopdc  16467  uspgr1ewopdc  16468  usgr1eop  16469  usgr2v1e2w  16470  vdegp1aid  16538  vdegp1bid  16539  eupth2lemsfi  16702  konigsbergvtx  16706  konigsbergiedg  16707  konigsbergumgr  16711  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  konigsberglem5  16716  konigsberg  16717  isomninnlem  17053  trilpolemlt1  17064  iswomninnlem  17073  iswomni0  17075  ismkvnnlem  17076