Theorem prexg 4351

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 3823, prprc1 3821, and prprc2 3822. (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 3789	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2307	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 4349	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 2883	. . . 4 ⊢ (𝐵 ∈ 𝑊 → {𝑥, 𝐵} ∈ V)
5		preq1 3788	. . . . 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)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  Vcvv 2821  {cpr 3710

This proof depends on 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 4251  ax-pr 4348

This proof 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 3715  df-pr 3716

This theorem is used by:  prelpw  4355  prelpwi  4356  opexg  4370  opi2  4375  opth  4379  opeqsn  4395  opeqpr  4396  uniop  4398  unex  4589  tpexg  4592  op1stb  4626  op1stbg  4627  onun2  4639  opthreg  4705  relop  4932  acexmidlemv  6086  2oex  6708  en2prd  7111  pw2f1odclem  7139  pr2ne  7545  exmidonfinlem  7552  exmidaclem  7571  sup3exmid  9296  xrex  10276  2strbasg  13534  2stropg  13535  xpsfval  13729  prdsex  14280  prdsval  14281  xpsval  14309  struct2slots2dom  16496  structiedg0val  16498  edgstruct  16522  umgrbien  16568  upgr1edc  16579  upgr1eopdc  16581  uspgr1edc  16698  usgr1e  16699  uspgr1eopdc  16701  uspgr1ewopdc  16702  usgr1eop  16703  usgr2v1e2w  16704  vdegp1aid  16772  vdegp1bid  16773  eupth2lemsfi  16936  konigsbergvtx  16940  konigsbergiedg  16941  konigsbergumgr  16945  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  konigsberglem5  16950  konigsberg  16951  isomninnlem  17297  trilpolemlt1  17309  iswomninnlem  17318  iswomni0  17320  ismkvnnlem  17321