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

Theorem prexg 4166
 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 3665, prprc1 3663, and prprc2 3664. (Contributed by Jim Kingdon, 16-Sep-2018.)
Assertion
Ref Expression
prexg

Proof of Theorem prexg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq2 3633 . . . . . 6
21eleq1d 2223 . . . . 5
3 zfpair2 4165 . . . . 5
42, 3vtoclg 2769 . . . 4
5 preq1 3632 . . . . 5
65eleq1d 2223 . . . 4
74, 6syl5ib 153 . . 3
87vtocleg 2780 . 2
98imp 123 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wceq 1332   wcel 2125  cvv 2709  cpr 3557 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 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-pr 4164 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-v 2711  df-un 3102  df-sn 3562  df-pr 3563 This theorem is referenced by:  prelpwi  4169  opexg  4183  opi2  4188  opth  4192  opeqsn  4207  opeqpr  4208  uniop  4210  unex  4395  tpexg  4398  op1stb  4432  op1stbg  4433  onun2  4443  opthreg  4509  relop  4729  acexmidlemv  5812  pr2ne  7106  exmidonfinlem  7107  exmidaclem  7122  sup3exmid  8807  xrex  9738  2strbasg  12230  2stropg  12231  isomninnlem  13542  trilpolemlt1  13553  iswomninnlem  13561  iswomni0  13563  ismkvnnlem  13564
 Copyright terms: Public domain W3C validator