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

Theorem prexg 4255
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 3743, prprc1 3741, and prprc2 3742. (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 3711 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2274 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4254 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 2833 . . . 4  |-  ( B  e.  W  ->  { x ,  B }  e.  _V )
5 preq1 3710 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2274 . . . 4  |-  ( x  =  A  ->  ( { x ,  B }  e.  _V  <->  { A ,  B }  e.  _V ) )
74, 6imbitrid 154 . . 3  |-  ( x  =  A  ->  ( B  e.  W  ->  { A ,  B }  e.  _V ) )
87vtocleg 2844 . 2  |-  ( A  e.  V  ->  ( B  e.  W  ->  { A ,  B }  e.  _V ) )
98imp 124 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  { A ,  B }  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    = wceq 1373    e. wcel 2176   _Vcvv 2772   {cpr 3634
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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pr 4253
This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640
This theorem is referenced by:  prelpwi  4258  opexg  4272  opi2  4277  opth  4281  opeqsn  4297  opeqpr  4298  uniop  4300  unex  4488  tpexg  4491  op1stb  4525  op1stbg  4526  onun2  4538  opthreg  4604  relop  4828  acexmidlemv  5942  en2prd  6909  pw2f1odclem  6931  pr2ne  7300  exmidonfinlem  7301  exmidaclem  7320  sup3exmid  9030  xrex  9978  2strbasg  12952  2stropg  12953  prdsex  13101  prdsval  13105  xpsfval  13180  xpsval  13184  gsumprval  13231  struct2slots2dom  15635  structiedg0val  15637  edgstruct  15656  isomninnlem  15969  trilpolemlt1  15980  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991
  Copyright terms: Public domain W3C validator