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

Theorem opex 4174
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 3734 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 prex 4155 . . 3  |-  { { A } ,  { A ,  B } }  e.  _V
3 0ex 4090 . . 3  |-  (/)  e.  _V
42, 3ifex 3564 . 2  |-  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )  e. 
_V
51, 4eqeltri 2326 1  |-  <. A ,  B >.  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 360    e. wcel 1621   _Vcvv 2740   (/)c0 3397   ifcif 3506   {csn 3581   {cpr 3582   <.cop 3584
This theorem is referenced by:  otex  4175  otth2  4186  oteqex2  4195  oteqex  4196  euop2  4203  opabid  4208  elopab  4209  opabn0  4232  opeliunxp  4693  elvvv  4702  opbrop  4720  relsnop  4744  xpiindi  4774  raliunxp  4778  intirr  5014  xpnz  5052  dmsnn0  5090  dmsnopg  5096  cnvcnvsn  5102  op2ndb  5108  opswap  5111  cnviin  5164  funopg  5190  dffv2  5491  fsn  5595  fvsn  5612  resfunexg  5636  idref  5658  fveqf1o  5705  fliftel  5707  fliftel1  5708  oprabid  5781  dfoprab2  5794  rnoprab  5829  eloprabga  5833  ot1stg  6033  ot2ndg  6034  ot3rdg  6035  fo1st  6038  fo2nd  6039  eloprabi  6085  fpar  6121  algrflem  6123  frxp  6124  xporderlem  6125  fnwelem  6129  brtpos  6142  dmtpos  6145  rntpos  6146  tpostpos  6153  opiota  6221  tfrlem11  6337  seqomlem1  6395  seqomlem3  6397  seqomlem4  6398  omeu  6516  iiner  6664  th3qlem2  6698  xpsnen  6879  xpcomco  6885  xpassen  6889  xpmapenlem  6961  unxpdomlem1  7000  fseqenlem2  7585  cda1dif  7735  fpwwe  8201  addpipq2  8493  addpqnq  8495  mulpipq2  8496  mulpqnq  8498  ordpipq  8499  prlem934  8590  addsrpr  8630  mulsrpr  8631  addcnsr  8690  mulcnsr  8691  ltresr  8695  addcnsrec  8698  mulcnsrec  8699  axcnre  8719  om2uzrdg  10950  uzrdg0i  10953  uzrdgsuci  10954  hashfun  11319  s1len  11374  s111  11378  wrdexb  11379  fsumcnv  12166  ruclem1  12436  ruclem4  12439  eucalgval2  12678  crt  12773  phimullem  12774  setsval  13099  setsres  13101  setscom  13103  strfv  13107  setsid  13114  imasaddfnlem  13357  imasaddvallem  13358  imasvscafn  13366  idfuval  13677  cofuval  13683  resfval  13693  resfval2  13694  elhoma  13791  xpcco  13884  xpcid  13890  1stfval  13892  2ndfval  13895  prfval  13900  prf1  13901  prf2  13903  evlfval  13918  curfval  13924  curf1  13926  curfcl  13933  hofval  13953  grpss  14430  efgmval  14948  efgi  14955  efgi2  14961  frgpnabllem1  15088  frgpnabllem2  15089  opsrtoslem2  16153  txcnp  17241  upxp  17244  uptx  17246  txdis1cn  17256  hauseqlcld  17267  txlm  17269  xkoinjcn  17308  txflf  17628  divstgplem  17730  imasdsf1olem  17864  cnheiborlem  18379  ovollb2lem  18774  ovolctb  18776  ovolshftlem1  18795  ovolscalem1  18799  ovolicc1  18802  ioombl1lem3  18844  ioombl1lem4  18845  ioorval  18856  dyadval  18874  mbfimaopnlem  18937  limccnp2  19169  ex-br  20726  grposn  20807  gidsn  20940  ginvsn  20941  rngosn  20996  rngosn3  21018  zrdivrng  21024  cnnvg  21171  cnnvs  21174  cnnvnm  21175  h2hva  21479  h2hsm  21480  h2hnm  21481  hhssva  21761  hhsssm  21762  hhssnm  21763  hhshsslem1  21769  erdszelem9  23067  erdszelem10  23068  txpcon  23100  txsconlem  23108  ghomsn  23332  brtpid1  23412  brtpid2  23413  brtpid3  23414  brtp  23442  dfpo2  23448  br8  23449  br6  23450  br4  23451  br1steq  23464  br2ndeq  23465  dfdm5  23466  dfrn5  23467  wfrlem14  23603  brv  23758  brtxp  23761  brpprod  23766  brpprod3b  23768  brsset  23770  brtxpsd  23775  elfuns  23794  brcart  23811  brimg  23816  brapply  23817  brcup  23818  brcap  23819  brsuccf  23820  brrestrict  23827  dfrdg4  23828  tfrqfree  23829  brbtwn  23867  brcgr  23868  fvtransport  23995  brcolinear2  24021  colineardim1  24024  brsegle  24071  fvline  24107  ellines  24115  elo  24372  prj1b  24410  prj3  24411  eloi  24417  domintrefc  24457  cbcpcp  24494  exopcopn  24904  1alg  25054  1ded  25070  1cat  25091  idmor  25278  domidmor  25280  codidmor  25282  grphidmor  25284  grphidmor2  25285  cmp2morp  25290  cmp2morpgrp  25295  cmp2morpdom  25296  cmp2morpcod  25297  cmppar2  25304  iscatset  25310  filnetlem3  25661  heiborlem6  25872  heiborlem7  25873  heiborlem8  25874  bnj97  27910  bnj553  27942  bnj966  27988  bnj1442  28091  dvhvaddval  30410  dvhvscaval  30419  dibglbN  30486  dihglbcpreN  30620  dihmeetlem4preN  30626  dihmeetlem13N  30639  hdmapfval  31150
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 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590
  Copyright terms: Public domain W3C validator