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

Theorem opexg 3991
Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)
Assertion
Ref Expression
opexg  |-  ( ( A  e.  V  /\  B  e.  W )  -> 
<. A ,  B >.  e. 
_V )

Proof of Theorem opexg
StepHypRef Expression
1 dfopg 3576 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  -> 
<. A ,  B >.  =  { { A } ,  { A ,  B } } )
2 elex 2611 . . . . 5  |-  ( A  e.  V  ->  A  e.  _V )
3 snexg 3964 . . . . 5  |-  ( A  e.  _V  ->  { A }  e.  _V )
42, 3syl 14 . . . 4  |-  ( A  e.  V  ->  { A }  e.  _V )
54adantr 270 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  { A }  e.  _V )
6 elex 2611 . . . 4  |-  ( B  e.  W  ->  B  e.  _V )
7 prexg 3974 . . . 4  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  { A ,  B }  e.  _V )
82, 6, 7syl2an 283 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  { A ,  B }  e.  _V )
9 prexg 3974 . . 3  |-  ( ( { A }  e.  _V  /\  { A ,  B }  e.  _V )  ->  { { A } ,  { A ,  B } }  e.  _V )
105, 8, 9syl2anc 403 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  { { A } ,  { A ,  B } }  e.  _V )
111, 10eqeltrd 2156 1  |-  ( ( A  e.  V  /\  B  e.  W )  -> 
<. A ,  B >.  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1434   _Vcvv 2602   {csn 3406   {cpr 3407   <.cop 3409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-pow 3956  ax-pr 3972
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-pw 3392  df-sn 3412  df-pr 3413  df-op 3415
This theorem is referenced by:  opex  3992  otexg  3993  opeliunxp  4421  opbrop  4445  relsnopg  4470  opswapg  4837  elxp4  4838  elxp5  4839  resfunexg  5414  fliftel  5464  fliftel1  5465  oprabid  5568  ovexg  5570  eloprabga  5622  op1st  5804  op2nd  5805  ot1stg  5810  ot2ndg  5811  ot3rdgg  5812  elxp6  5827  mpt2fvex  5860  algrflem  5881  algrflemg  5882  mpt2xopoveq  5889  brtposg  5903  tfr0dm  5971  tfrlemisucaccv  5974  tfrlemibxssdm  5976  tfrlemibfn  5977  tfrlemi14d  5982  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemres  5998  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemres  6011  fnfi  6446  mulpipq2  6623  enq0breq  6688  addvalex  7074  peano2nnnn  7083  axcnre  7109  frec2uzrdg  9491  frecuzrdg0  9495  frecuzrdgg  9498  frecuzrdg0t  9504  eucalgval2  10579
  Copyright terms: Public domain W3C validator