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

Theorem prexg 4101
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 3601, prprc1 3599, and prprc2 3600. (Contributed by Jim Kingdon, 16-Sep-2018.)
Assertion
Ref Expression
prexg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  { A ,  B }  e.  _V )

Proof of Theorem prexg
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq2 3569 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2184 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4100 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 2718 . . . 4  |-  ( B  e.  W  ->  { x ,  B }  e.  _V )
5 preq1 3568 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2184 . . . 4  |-  ( x  =  A  ->  ( { x ,  B }  e.  _V  <->  { A ,  B }  e.  _V ) )
74, 6syl5ib 153 . . 3  |-  ( x  =  A  ->  ( B  e.  W  ->  { A ,  B }  e.  _V ) )
87vtocleg 2729 . 2  |-  ( A  e.  V  ->  ( B  e.  W  ->  { A ,  B }  e.  _V ) )
98imp 123 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  { A ,  B }  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1314    e. wcel 1463   _Vcvv 2658   {cpr 3496
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502
This theorem is referenced by:  prelpwi  4104  opexg  4118  opi2  4123  opth  4127  opeqsn  4142  opeqpr  4143  uniop  4145  unex  4330  tpexg  4333  op1stb  4367  op1stbg  4368  onun2  4374  opthreg  4439  relop  4657  acexmidlemv  5738  pr2ne  7014  exmidaclem  7028  sup3exmid  8672  xrex  9579  2strbasg  11955  2stropg  11956  isomninnlem  13036  trilpolemlt1  13045
  Copyright terms: Public domain W3C validator