MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opex Unicode version

Theorem opex 4237
Description: An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opex  |-  <. A ,  B >.  e.  _V

Proof of Theorem opex
StepHypRef Expression
1 dfopif 3793 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 prex 4217 . . 3  |-  { { A } ,  { A ,  B } }  e.  _V
3 0ex 4150 . . 3  |-  (/)  e.  _V
42, 3ifex 3623 . 2  |-  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )  e. 
_V
51, 4eqeltri 2353 1  |-  <. A ,  B >.  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1684   _Vcvv 2788   (/)c0 3455   ifcif 3565   {csn 3640   {cpr 3641   <.cop 3643
This theorem is referenced by:  otex  4238  otth2  4249  oteqex2  4258  oteqex  4259  euop2  4266  opabid  4271  elopab  4272  opabn0  4295  opeliunxp  4740  elvvv  4749  opbrop  4767  relsnop  4791  xpiindi  4821  raliunxp  4825  intirr  5061  xpnz  5099  dmsnn0  5138  dmsnopg  5144  cnvcnvsn  5150  op2ndb  5156  opswap  5159  cnviin  5212  funopg  5286  dffv2  5592  fsn  5696  fvsn  5713  resfunexg  5737  idref  5759  fveqf1o  5806  fliftel  5808  fliftel1  5809  oprabid  5882  dfoprab2  5895  rnoprab  5930  eloprabga  5934  ot1stg  6134  ot2ndg  6135  ot3rdg  6136  fo1st  6139  fo2nd  6140  eloprabi  6186  fpar  6222  algrflem  6224  frxp  6225  xporderlem  6226  fnwelem  6230  brtpos  6243  dmtpos  6246  rntpos  6247  tpostpos  6254  opiota  6290  tfrlem11  6404  seqomlem1  6462  seqomlem3  6464  seqomlem4  6465  omeu  6583  iiner  6731  th3qlem2  6765  xpsnen  6946  xpcomco  6952  xpassen  6956  xpmapenlem  7028  unxpdomlem1  7067  fseqenlem2  7652  cda1dif  7802  fpwwe  8268  addpipq2  8560  addpqnq  8562  mulpipq2  8563  mulpqnq  8565  ordpipq  8566  prlem934  8657  addsrpr  8697  mulsrpr  8698  addcnsr  8757  mulcnsr  8758  ltresr  8762  addcnsrec  8765  mulcnsrec  8766  axcnre  8786  om2uzrdg  11019  uzrdg0i  11022  uzrdgsuci  11023  hashfun  11389  s1len  11444  s111  11448  wrdexb  11449  fsumcnv  12236  ruclem1  12509  ruclem4  12512  eucalgval2  12751  crt  12846  phimullem  12847  setsval  13172  setsres  13174  setscom  13176  strfv  13180  setsid  13187  imasaddfnlem  13430  imasaddvallem  13431  imasvscafn  13439  idfuval  13750  cofuval  13756  resfval  13766  resfval2  13767  elhoma  13864  xpcco  13957  xpcid  13963  1stfval  13965  2ndfval  13968  prfval  13973  prf1  13974  prf2  13976  evlfval  13991  curfval  13997  curf1  13999  curfcl  14006  hofval  14026  grpss  14503  efgmval  15021  efgi  15028  efgi2  15034  frgpnabllem1  15161  frgpnabllem2  15162  opsrtoslem2  16226  txcnp  17314  upxp  17317  uptx  17319  txdis1cn  17329  hauseqlcld  17340  txlm  17342  xkoinjcn  17381  txflf  17701  divstgplem  17803  imasdsf1olem  17937  cnheiborlem  18452  ovollb2lem  18847  ovolctb  18849  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ioombl1lem3  18917  ioombl1lem4  18918  ioorval  18929  dyadval  18947  mbfimaopnlem  19010  limccnp2  19242  ex-br  20818  grposn  20882  gidsn  21015  ginvsn  21016  rngosn  21071  rngosn3  21093  zrdivrng  21099  cnnvg  21246  cnnvs  21249  cnnvnm  21250  h2hva  21554  h2hsm  21555  h2hnm  21556  hhssva  21836  hhsssm  21837  hhssnm  21838  hhshsslem1  21844  xppreima2  23212  erdszelem9  23730  erdszelem10  23731  txpcon  23763  txsconlem  23771  ghomsn  23995  brtpid1  24075  brtpid2  24076  brtpid3  24077  brtp  24106  dfpo2  24112  br8  24113  br6  24114  br4  24115  br1steq  24130  br2ndeq  24131  dfdm5  24132  dfrn5  24133  wfrlem14  24269  brv  24417  brtxp  24420  brpprod  24425  brpprod3b  24427  brsset  24429  brtxpsd  24434  brcart  24471  brimg  24476  brapply  24477  brcup  24478  brcap  24479  brsuccf  24480  brrestrict  24487  dfrdg4  24488  tfrqfree  24489  brbtwn  24527  brcgr  24528  fvtransport  24655  brcolinear2  24681  colineardim1  24684  brsegle  24731  fvline  24767  ellines  24775  elo  25041  prj1b  25079  prj3  25080  eloi  25086  domintrefc  25125  cbcpcp  25162  exopcopn  25572  1alg  25722  1ded  25738  1cat  25759  idmor  25946  domidmor  25948  codidmor  25950  grphidmor  25952  grphidmor2  25953  cmp2morp  25958  cmp2morpgrp  25963  cmp2morpdom  25964  cmp2morpcod  25965  cmppar2  25972  iscatset  25978  filnetlem3  26329  heiborlem6  26540  heiborlem7  26541  heiborlem8  26542  mpt2xopoveq  28085  nbgraop  28140  bnj97  28898  bnj553  28930  bnj966  28976  bnj1442  29079  dvhvaddval  31280  dvhvscaval  31289  dibglbN  31356  dihglbcpreN  31490  dihmeetlem4preN  31496  dihmeetlem13N  31509  hdmapfval  32020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649
  Copyright terms: Public domain W3C validator