Theorem prexg 4349

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 4347	. . . . 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 4249  ax-pr 4346

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  4353  prelpwi  4354  opexg  4368  opi2  4373  opth  4377  opeqsn  4393  opeqpr  4394  uniop  4396  unex  4587  tpexg  4590  op1stb  4624  op1stbg  4625  onun2  4637  opthreg  4703  relop  4930  acexmidlemv  6083  2oex  6704  en2prd  7106  pw2f1odclem  7134  pr2ne  7538  exmidonfinlem  7545  exmidaclem  7564  sup3exmid  9288  xrex  10260  2strbasg  13476  2stropg  13477  xpsfval  13671  prdsex  14174  prdsval  14175  xpsval  14203  struct2slots2dom  16291  structiedg0val  16293  edgstruct  16317  umgrbien  16363  upgr1edc  16374  upgr1eopdc  16376  uspgr1edc  16493  usgr1e  16494  uspgr1eopdc  16496  uspgr1ewopdc  16497  usgr1eop  16498  usgr2v1e2w  16499  vdegp1aid  16567  vdegp1bid  16568  eupth2lemsfi  16731  konigsbergvtx  16735  konigsbergiedg  16736  konigsbergumgr  16740  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  konigsberglem5  16745  konigsberg  16746  isomninnlem  17091  trilpolemlt1  17102  iswomninnlem  17111  iswomni0  17113  ismkvnnlem  17114