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

Theorem opex 4209
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 3767 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 prex 4189 . . 3  |-  { { A } ,  { A ,  B } }  e.  _V
3 0ex 4124 . . 3  |-  (/)  e.  _V
42, 3ifex 3597 . 2  |-  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )  e. 
_V
51, 4eqeltri 2328 1  |-  <. A ,  B >.  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 360    e. wcel 1621   _Vcvv 2763   (/)c0 3430   ifcif 3539   {csn 3614   {cpr 3615   <.cop 3617
This theorem is referenced by:  otex  4210  otth2  4221  oteqex2  4230  oteqex  4231  euop2  4238  opabid  4243  elopab  4244  opabn0  4267  opeliunxp  4728  elvvv  4737  opbrop  4755  relsnop  4779  xpiindi  4809  raliunxp  4813  intirr  5049  xpnz  5087  dmsnn0  5125  dmsnopg  5131  cnvcnvsn  5137  op2ndb  5143  opswap  5146  cnviin  5199  funopg  5225  dffv2  5526  fsn  5630  fvsn  5647  resfunexg  5671  idref  5693  fveqf1o  5740  fliftel  5742  fliftel1  5743  oprabid  5816  dfoprab2  5829  rnoprab  5864  eloprabga  5868  ot1stg  6068  ot2ndg  6069  ot3rdg  6070  fo1st  6073  fo2nd  6074  eloprabi  6120  fpar  6156  algrflem  6158  frxp  6159  xporderlem  6160  fnwelem  6164  brtpos  6177  dmtpos  6180  rntpos  6181  tpostpos  6188  opiota  6256  tfrlem11  6372  seqomlem1  6430  seqomlem3  6432  seqomlem4  6433  omeu  6551  iiner  6699  th3qlem2  6733  xpsnen  6914  xpcomco  6920  xpassen  6924  xpmapenlem  6996  unxpdomlem1  7035  fseqenlem2  7620  cda1dif  7770  fpwwe  8236  addpipq2  8528  addpqnq  8530  mulpipq2  8531  mulpqnq  8533  ordpipq  8534  prlem934  8625  addsrpr  8665  mulsrpr  8666  addcnsr  8725  mulcnsr  8726  ltresr  8730  addcnsrec  8733  mulcnsrec  8734  axcnre  8754  om2uzrdg  10985  uzrdg0i  10988  uzrdgsuci  10989  hashfun  11354  s1len  11409  s111  11413  wrdexb  11414  fsumcnv  12201  ruclem1  12471  ruclem4  12474  eucalgval2  12713  crt  12808  phimullem  12809  setsval  13134  setsres  13136  setscom  13138  strfv  13142  setsid  13149  imasaddfnlem  13392  imasaddvallem  13393  imasvscafn  13401  idfuval  13712  cofuval  13718  resfval  13728  resfval2  13729  elhoma  13826  xpcco  13919  xpcid  13925  1stfval  13927  2ndfval  13930  prfval  13935  prf1  13936  prf2  13938  evlfval  13953  curfval  13959  curf1  13961  curfcl  13968  hofval  13988  grpss  14465  efgmval  14983  efgi  14990  efgi2  14996  frgpnabllem1  15123  frgpnabllem2  15124  opsrtoslem2  16188  txcnp  17276  upxp  17279  uptx  17281  txdis1cn  17291  hauseqlcld  17302  txlm  17304  xkoinjcn  17343  txflf  17663  divstgplem  17765  imasdsf1olem  17899  cnheiborlem  18414  ovollb2lem  18809  ovolctb  18811  ovolshftlem1  18830  ovolscalem1  18834  ovolicc1  18837  ioombl1lem3  18879  ioombl1lem4  18880  ioorval  18891  dyadval  18909  mbfimaopnlem  18972  limccnp2  19204  ex-br  20761  grposn  20842  gidsn  20975  ginvsn  20976  rngosn  21031  rngosn3  21053  zrdivrng  21059  cnnvg  21206  cnnvs  21209  cnnvnm  21210  h2hva  21514  h2hsm  21515  h2hnm  21516  hhssva  21796  hhsssm  21797  hhssnm  21798  hhshsslem1  21804  erdszelem9  23102  erdszelem10  23103  txpcon  23135  txsconlem  23143  ghomsn  23367  brtpid1  23447  brtpid2  23448  brtpid3  23449  brtp  23477  dfpo2  23483  br8  23484  br6  23485  br4  23486  br1steq  23499  br2ndeq  23500  dfdm5  23501  dfrn5  23502  wfrlem14  23638  brv  23793  brtxp  23796  brpprod  23801  brpprod3b  23803  brsset  23805  brtxpsd  23810  elfuns  23829  brcart  23846  brimg  23851  brapply  23852  brcup  23853  brcap  23854  brsuccf  23855  brrestrict  23862  dfrdg4  23863  tfrqfree  23864  brbtwn  23902  brcgr  23903  fvtransport  24030  brcolinear2  24056  colineardim1  24059  brsegle  24106  fvline  24142  ellines  24150  elo  24407  prj1b  24445  prj3  24446  eloi  24452  domintrefc  24492  cbcpcp  24529  exopcopn  24939  1alg  25089  1ded  25105  1cat  25126  idmor  25313  domidmor  25315  codidmor  25317  grphidmor  25319  grphidmor2  25320  cmp2morp  25325  cmp2morpgrp  25330  cmp2morpdom  25331  cmp2morpcod  25332  cmppar2  25339  iscatset  25345  filnetlem3  25696  heiborlem6  25907  heiborlem7  25908  heiborlem8  25909  bnj97  27947  bnj553  27979  bnj966  28025  bnj1442  28128  dvhvaddval  30447  dvhvscaval  30456  dibglbN  30523  dihglbcpreN  30657  dihmeetlem4preN  30663  dihmeetlem13N  30676  hdmapfval  31187
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623
  Copyright terms: Public domain W3C validator