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

Theorem opex 4238
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 3796 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 prex 4218 . . 3  |-  { { A } ,  { A ,  B } }  e.  _V
3 0ex 4153 . . 3  |-  (/)  e.  _V
42, 3ifex 3626 . 2  |-  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )  e. 
_V
51, 4eqeltri 2356 1  |-  <. A ,  B >.  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 360    e. wcel 1687   _Vcvv 2791   (/)c0 3458   ifcif 3568   {csn 3643   {cpr 3644   <.cop 3646
This theorem is referenced by:  otex  4239  otth2  4250  oteqex2  4259  oteqex  4260  euop2  4267  opabid  4272  elopab  4273  opabn0  4296  opeliunxp  4741  elvvv  4750  opbrop  4768  relsnop  4792  xpiindi  4822  raliunxp  4826  intirr  5062  xpnz  5100  dmsnn0  5138  dmsnopg  5144  cnvcnvsn  5150  op2ndb  5156  opswap  5159  cnviin  5212  funopg  5254  dffv2  5555  fsn  5659  fvsn  5676  resfunexg  5700  idref  5722  fveqf1o  5769  fliftel  5771  fliftel1  5772  oprabid  5845  dfoprab2  5858  rnoprab  5893  eloprabga  5897  ot1stg  6097  ot2ndg  6098  ot3rdg  6099  fo1st  6102  fo2nd  6103  eloprabi  6149  fpar  6185  algrflem  6187  frxp  6188  xporderlem  6189  fnwelem  6193  brtpos  6206  dmtpos  6209  rntpos  6210  tpostpos  6217  opiota  6285  tfrlem11  6401  seqomlem1  6459  seqomlem3  6461  seqomlem4  6462  omeu  6580  iiner  6728  th3qlem2  6762  xpsnen  6943  xpcomco  6949  xpassen  6953  xpmapenlem  7025  unxpdomlem1  7064  fseqenlem2  7649  cda1dif  7799  fpwwe  8265  addpipq2  8557  addpqnq  8559  mulpipq2  8560  mulpqnq  8562  ordpipq  8563  prlem934  8654  addsrpr  8694  mulsrpr  8695  addcnsr  8754  mulcnsr  8755  ltresr  8759  addcnsrec  8762  mulcnsrec  8763  axcnre  8783  om2uzrdg  11015  uzrdg0i  11018  uzrdgsuci  11019  hashfun  11385  s1len  11440  s111  11444  wrdexb  11445  fsumcnv  12232  ruclem1  12505  ruclem4  12508  eucalgval2  12747  crt  12842  phimullem  12843  setsval  13168  setsres  13170  setscom  13172  strfv  13176  setsid  13183  imasaddfnlem  13426  imasaddvallem  13427  imasvscafn  13435  idfuval  13746  cofuval  13752  resfval  13762  resfval2  13763  elhoma  13860  xpcco  13953  xpcid  13959  1stfval  13961  2ndfval  13964  prfval  13969  prf1  13970  prf2  13972  evlfval  13987  curfval  13993  curf1  13995  curfcl  14002  hofval  14022  grpss  14499  efgmval  15017  efgi  15024  efgi2  15030  frgpnabllem1  15157  frgpnabllem2  15158  opsrtoslem2  16222  txcnp  17310  upxp  17313  uptx  17315  txdis1cn  17325  hauseqlcld  17336  txlm  17338  xkoinjcn  17377  txflf  17697  divstgplem  17799  imasdsf1olem  17933  cnheiborlem  18448  ovollb2lem  18843  ovolctb  18845  ovolshftlem1  18864  ovolscalem1  18868  ovolicc1  18871  ioombl1lem3  18913  ioombl1lem4  18914  ioorval  18925  dyadval  18943  mbfimaopnlem  19006  limccnp2  19238  ex-br  20795  grposn  20876  gidsn  21009  ginvsn  21010  rngosn  21065  rngosn3  21087  zrdivrng  21093  cnnvg  21240  cnnvs  21243  cnnvnm  21244  h2hva  21548  h2hsm  21549  h2hnm  21550  hhssva  21830  hhsssm  21831  hhssnm  21832  hhshsslem1  21838  erdszelem9  23136  erdszelem10  23137  txpcon  23169  txsconlem  23177  ghomsn  23401  brtpid1  23481  brtpid2  23482  brtpid3  23483  brtp  23511  dfpo2  23517  br8  23518  br6  23519  br4  23520  br1steq  23533  br2ndeq  23534  dfdm5  23535  dfrn5  23536  wfrlem14  23672  brv  23827  brtxp  23830  brpprod  23835  brpprod3b  23837  brsset  23839  brtxpsd  23844  elfuns  23863  brcart  23880  brimg  23885  brapply  23886  brcup  23887  brcap  23888  brsuccf  23889  brrestrict  23896  dfrdg4  23897  tfrqfree  23898  brbtwn  23936  brcgr  23937  fvtransport  24064  brcolinear2  24090  colineardim1  24093  brsegle  24140  fvline  24176  ellines  24184  elo  24441  prj1b  24479  prj3  24480  eloi  24486  domintrefc  24526  cbcpcp  24563  exopcopn  24973  1alg  25123  1ded  25139  1cat  25160  idmor  25347  domidmor  25349  codidmor  25351  grphidmor  25353  grphidmor2  25354  cmp2morp  25359  cmp2morpgrp  25364  cmp2morpdom  25365  cmp2morpcod  25366  cmppar2  25373  iscatset  25379  filnetlem3  25730  heiborlem6  25941  heiborlem7  25942  heiborlem8  25943  bnj97  28167  bnj553  28199  bnj966  28245  bnj1442  28348  dvhvaddval  30549  dvhvscaval  30558  dibglbN  30625  dihglbcpreN  30759  dihmeetlem4preN  30765  dihmeetlem13N  30778  hdmapfval  31289
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-sep 4144  ax-nul 4152  ax-pr 4215
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-v 2793  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-nul 3459  df-if 3569  df-sn 3649  df-pr 3650  df-op 3652
  Copyright terms: Public domain W3C validator