Theorem prexg 4324

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 3801, prprc1 3799, and prprc2 3800. (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 3768	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2301	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 4322	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 2874	. . . 4 ⊢ (𝐵 ∈ 𝑊 → {𝑥, 𝐵} ∈ V)
5		preq1 3767	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2301	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 154	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ 𝑊 → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 2887	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → {𝐴, 𝐵} ∈ V))
9	8	imp 124	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2203  Vcvv 2812  {cpr 3689

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pr 4321

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-sn 3694  df-pr 3695

This theorem is referenced by:  prelpw  4328  prelpwi  4329  opexg  4343  opi2  4348  opth  4352  opeqsn  4368  opeqpr  4369  uniop  4371  unex  4561  tpexg  4564  op1stb  4598  op1stbg  4599  onun2  4611  opthreg  4677  relop  4904  acexmidlemv  6047  2oex  6663  en2prd  7058  pw2f1odclem  7086  pr2ne  7488  exmidonfinlem  7495  exmidaclem  7514  sup3exmid  9230  xrex  10188  2strbasg  13325  2stropg  13326  prdsex  13474  prdsval  13478  xpsfval  13553  xpsval  13557  gsumprval  13604  struct2slots2dom  16025  structiedg0val  16027  edgstruct  16051  umgrbien  16097  upgr1edc  16108  upgr1eopdc  16110  uspgr1edc  16227  usgr1e  16228  uspgr1eopdc  16230  uspgr1ewopdc  16231  usgr1eop  16232  usgr2v1e2w  16233  vdegp1aid  16301  vdegp1bid  16302  eupth2lemsfi  16465  konigsbergvtx  16469  konigsbergiedg  16470  konigsbergumgr  16474  konigsberglem1  16475  konigsberglem2  16476  konigsberglem3  16477  konigsberglem5  16479  konigsberg  16480  isomninnlem  16806  trilpolemlt1  16817  iswomninnlem  16826  iswomni0  16828  ismkvnnlem  16829