Theorem prexg 4299

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 3780, prprc1 3778, and prprc2 3779. (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 3747	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2298	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 4298	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 2862	. . . 4 ⊢ (𝐵 ∈ 𝑊 → {𝑥, 𝐵} ∈ V)
5		preq1 3746	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2298	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 154	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ 𝑊 → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 2875	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → {𝐴, 𝐵} ∈ V))
9	8	imp 124	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  Vcvv 2800  {cpr 3668

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pr 4297

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674

This theorem is referenced by:  prelpw  4303  prelpwi  4304  opexg  4318  opi2  4323  opth  4327  opeqsn  4343  opeqpr  4344  uniop  4346  unex  4536  tpexg  4539  op1stb  4573  op1stbg  4574  onun2  4586  opthreg  4652  relop  4878  acexmidlemv  6011  2oex  6594  en2prd  6987  pw2f1odclem  7015  pr2ne  7391  exmidonfinlem  7397  exmidaclem  7416  sup3exmid  9130  xrex  10084  2strbasg  13196  2stropg  13197  prdsex  13345  prdsval  13349  xpsfval  13424  xpsval  13428  gsumprval  13475  struct2slots2dom  15882  structiedg0val  15884  edgstruct  15908  umgrbien  15954  upgr1edc  15965  upgr1eopdc  15967  uspgr1edc  16084  usgr1e  16085  uspgr1eopdc  16087  uspgr1ewopdc  16088  usgr1eop  16089  usgr2v1e2w  16090  vdegp1aid  16125  vdegp1bid  16126  isomninnlem  16584  trilpolemlt1  16595  iswomninnlem  16603  iswomni0  16605  ismkvnnlem  16606