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

Theorem opex 4130
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 3693 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 prex 4111 . . 3  |-  { { A } ,  { A ,  B } }  e.  _V
3 0ex 4047 . . 3  |-  (/)  e.  _V
42, 3ifex 3528 . 2  |-  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )  e. 
_V
51, 4eqeltri 2323 1  |-  <. A ,  B >.  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 360    e. wcel 1621   _Vcvv 2727   (/)c0 3362   ifcif 3470   {csn 3544   {cpr 3545   <.cop 3547
This theorem is referenced by:  otex  4131  otth2  4142  oteqex2  4151  oteqex  4152  euop2  4159  opabid  4164  elopab  4165  opabn0  4188  opeliunxp  4647  elvvv  4656  opbrop  4674  relsnop  4698  xpiindi  4728  raliunxp  4732  intirr  4968  xpnz  5006  dmsnn0  5044  dmsnopg  5050  cnvcnvsn  5056  op2ndb  5062  opswap  5065  cnviin  5118  funopg  5144  dffv2  5444  fsn  5548  fvsn  5565  resfunexg  5589  idref  5611  fveqf1o  5658  fliftel  5660  fliftel1  5661  oprabid  5734  dfoprab2  5747  rnoprab  5782  eloprabga  5786  ot1stg  5986  ot2ndg  5987  ot3rdg  5988  fo1st  5991  fo2nd  5992  eloprabi  6038  fpar  6074  algrflem  6076  frxp  6077  xporderlem  6078  fnwelem  6082  brtpos  6095  dmtpos  6098  rntpos  6099  tpostpos  6106  opiota  6174  tfrlem11  6290  seqomlem1  6348  seqomlem3  6350  seqomlem4  6351  omeu  6469  iiner  6617  th3qlem2  6651  xpsnen  6831  xpcomco  6837  xpassen  6841  xpmapenlem  6913  unxpdomlem1  6952  fseqenlem2  7536  cda1dif  7686  fpwwe  8148  addpipq2  8440  addpqnq  8442  mulpipq2  8443  mulpqnq  8445  ordpipq  8446  prlem934  8537  addsrpr  8577  mulsrpr  8578  addcnsr  8637  mulcnsr  8638  ltresr  8642  addcnsrec  8645  mulcnsrec  8646  axcnre  8666  om2uzrdg  10897  uzrdg0i  10900  uzrdgsuci  10901  hashfun  11266  s1len  11321  s111  11325  wrdexb  11326  fsumcnv  12113  ruclem1  12383  ruclem4  12386  eucalgval2  12625  crt  12720  phimullem  12721  setsval  13046  setsres  13048  setscom  13050  strfv  13054  setsid  13061  imasaddfnlem  13304  imasaddvallem  13305  imasvscafn  13313  idfuval  13594  cofuval  13600  resfval  13610  resfval2  13611  elhoma  13708  xpcco  13801  xpcid  13807  1stfval  13809  2ndfval  13812  prfval  13817  prf1  13818  prf2  13820  evlfval  13835  curfval  13841  curf1  13843  curfcl  13850  hofval  13870  grpss  14338  efgmval  14856  efgi  14863  efgi2  14869  frgpnabllem1  14996  frgpnabllem2  14997  opsrtoslem2  16058  txcnp  17146  upxp  17149  uptx  17151  txdis1cn  17161  hauseqlcld  17172  txlm  17174  xkoinjcn  17213  txflf  17533  divstgplem  17635  imasdsf1olem  17769  cnheiborlem  18284  ovollb2lem  18679  ovolctb  18681  ovolshftlem1  18700  ovolscalem1  18704  ovolicc1  18707  ioombl1lem3  18749  ioombl1lem4  18750  ioorval  18761  dyadval  18779  mbfimaopnlem  18842  limccnp2  19074  ex-br  20631  grposn  20712  gidsn  20845  ginvsn  20846  rngosn  20901  rngosn3  20923  zrdivrng  20929  cnnvg  21076  cnnvs  21079  cnnvnm  21080  h2hva  21384  h2hsm  21385  h2hnm  21386  hhssva  21666  hhsssm  21667  hhssnm  21668  hhshsslem1  21674  erdszelem9  22901  erdszelem10  22902  txpcon  22934  txsconlem  22942  ghomsn  23166  brtpid1  23246  brtpid2  23247  brtpid3  23248  brtp  23276  dfpo2  23282  br8  23283  br6  23284  br4  23285  br1steq  23298  br2ndeq  23299  dfdm5  23300  dfrn5  23301  wfrlem14  23437  brv  23592  brtxp  23595  brpprod  23600  brpprod3b  23602  brsset  23604  brtxpsd  23609  elfuns  23628  brcart  23645  brimg  23650  brapply  23651  brcup  23652  brcap  23653  brsuccf  23654  brrestrict  23661  dfrdg4  23662  tfrqfree  23663  brbtwn  23701  brcgr  23702  fvtransport  23829  brcolinear2  23855  colineardim1  23858  brsegle  23905  fvline  23941  ellines  23949  elo  24206  prj1b  24244  prj3  24245  eloi  24251  domintrefc  24291  cbcpcp  24328  exopcopn  24738  1alg  24888  1ded  24904  1cat  24925  idmor  25112  domidmor  25114  codidmor  25116  grphidmor  25118  grphidmor2  25119  cmp2morp  25124  cmp2morpgrp  25129  cmp2morpdom  25130  cmp2morpcod  25131  cmppar2  25138  iscatset  25144  filnetlem3  25495  heiborlem6  25706  heiborlem7  25707  heiborlem8  25708  bnj97  27587  bnj553  27619  bnj966  27665  bnj1442  27768  dvhvaddval  30081  dvhvscaval  30090  dibglbN  30157  dihglbcpreN  30291  dihmeetlem4preN  30297  dihmeetlem13N  30310  hdmapfval  30821
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553
  Copyright terms: Public domain W3C validator