Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  prexg GIF version

Theorem prexg 4143
 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 3642, prprc1 3640, and prprc2 3641. (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.
StepHypRef Expression
1 preq2 3610 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2209 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 4142 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 2750 . . . 4 (𝐵𝑊 → {𝑥, 𝐵} ∈ V)
5 preq1 3609 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2209 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6syl5ib 153 . . 3 (𝑥 = 𝐴 → (𝐵𝑊 → {𝐴, 𝐵} ∈ V))
87vtocleg 2761 . 2 (𝐴𝑉 → (𝐵𝑊 → {𝐴, 𝐵} ∈ V))
98imp 123 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ V)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332   ∈ wcel 1481  Vcvv 2690  {cpr 3534 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pr 4141 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2692  df-un 3081  df-sn 3539  df-pr 3540 This theorem is referenced by:  prelpwi  4146  opexg  4160  opi2  4165  opth  4169  opeqsn  4184  opeqpr  4185  uniop  4187  unex  4372  tpexg  4375  op1stb  4409  op1stbg  4410  onun2  4416  opthreg  4481  relop  4700  acexmidlemv  5783  pr2ne  7075  exmidonfinlem  7076  exmidaclem  7091  sup3exmid  8766  xrex  9696  2strbasg  12133  2stropg  12134  isomninnlem  13443  trilpolemlt1  13454  iswomninnlem  13462  iswomni0  13464  ismkvnnlem  13465
 Copyright terms: Public domain W3C validator