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

Theorem opex 4274
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 3830 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 prex 4254 . . 3  |-  { { A } ,  { A ,  B } }  e.  _V
3 0ex 4187 . . 3  |-  (/)  e.  _V
42, 3ifex 3657 . 2  |-  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )  e. 
_V
51, 4eqeltri 2386 1  |-  <. A ,  B >.  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1701   _Vcvv 2822   (/)c0 3489   ifcif 3599   {csn 3674   {cpr 3675   <.cop 3677
This theorem is referenced by:  otex  4275  otth2  4286  oteqex2  4295  oteqex  4296  euop2  4303  opabid  4308  elopab  4309  opabn0  4332  opeliunxp  4777  elvvv  4786  opbrop  4804  relsnop  4828  xpiindi  4858  raliunxp  4862  intirr  5098  xpnz  5136  dmsnn0  5175  dmsnopg  5181  cnvcnvsn  5187  op2ndb  5193  opswap  5196  cnviin  5249  funopg  5323  dffv2  5630  fsn  5734  fvsn  5752  resfunexg  5778  idref  5800  fveqf1o  5848  fliftel  5850  fliftel1  5851  oprabid  5924  dfoprab2  5937  rnoprab  5972  eloprabga  5976  ot1stg  6176  ot2ndg  6177  ot3rdg  6178  fo1st  6181  fo2nd  6182  eloprabi  6228  fpar  6264  algrflem  6266  frxp  6267  xporderlem  6268  fnwelem  6272  brtpos  6285  dmtpos  6288  rntpos  6289  tpostpos  6296  opiota  6332  tfrlem11  6446  seqomlem1  6504  seqomlem3  6506  seqomlem4  6507  omeu  6625  iiner  6773  th3qlem2  6808  xpsnen  6989  xpcomco  6995  xpassen  6999  xpmapenlem  7071  unxpdomlem1  7110  fseqenlem2  7697  cda1dif  7847  fpwwe  8313  addpipq2  8605  addpqnq  8607  mulpipq2  8608  mulpqnq  8610  ordpipq  8611  prlem934  8702  addsrpr  8742  mulsrpr  8743  addcnsr  8802  mulcnsr  8803  ltresr  8807  addcnsrec  8810  mulcnsrec  8811  axcnre  8831  om2uzrdg  11066  uzrdg0i  11069  uzrdgsuci  11070  hashfun  11436  s1len  11491  s111  11495  wrdexb  11496  fsumcnv  12283  ruclem1  12556  ruclem4  12559  eucalgval2  12798  crt  12893  phimullem  12894  setsval  13219  setsres  13221  setscom  13223  strfv  13227  setsid  13234  imasaddfnlem  13479  imasaddvallem  13480  imasvscafn  13488  idfuval  13799  cofuval  13805  resfval  13815  resfval2  13816  elhoma  13913  xpcco  14006  xpcid  14012  1stfval  14014  2ndfval  14017  prfval  14022  prf1  14023  prf2  14025  evlfval  14040  curfval  14046  curf1  14048  curfcl  14055  hofval  14075  grpss  14552  efgmval  15070  efgi  15077  efgi2  15083  frgpnabllem1  15210  frgpnabllem2  15211  opsrtoslem2  16275  txcnp  17370  upxp  17373  uptx  17375  txdis1cn  17385  hauseqlcld  17396  txlm  17398  xkoinjcn  17437  txflf  17753  divstgplem  17855  imasdsf1olem  17989  cnheiborlem  18505  ovollb2lem  18900  ovolctb  18902  ovolshftlem1  18921  ovolscalem1  18925  ovolicc1  18928  ioombl1lem3  18970  ioombl1lem4  18971  ioorval  18982  dyadval  19000  mbfimaopnlem  19063  limccnp2  19295  ex-br  20871  grposn  20935  gidsn  21068  ginvsn  21069  rngosn  21124  rngosn3  21146  zrdivrng  21152  cnnvg  21301  cnnvs  21304  cnnvnm  21305  h2hva  21609  h2hsm  21610  h2hnm  21611  hhssva  21891  hhsssm  21892  hhssnm  21893  hhshsslem1  21899  xppreima2  23209  ucnima  23474  ucnprima  23475  fmucndlem  23483  fmucnd  23484  erdszelem9  24014  erdszelem10  24015  txpcon  24047  txsconlem  24055  ghomsn  24279  brtpid1  24359  brtpid2  24360  brtpid3  24361  brtp  24491  dfpo2  24497  br8  24498  br6  24499  br4  24500  br1steq  24515  br2ndeq  24516  dfdm5  24517  dfrn5  24518  wfrlem14  24654  brv  24802  brtxp  24805  brpprod  24810  brpprod3b  24812  brsset  24814  brtxpsd  24819  brcart  24856  brimg  24861  brapply  24862  brcup  24863  brcap  24864  brsuccf  24865  brrestrict  24873  dfrdg4  24874  tfrqfree  24875  brbtwn  24913  brcgr  24914  fvtransport  25041  brcolinear2  25067  colineardim1  25070  brsegle  25117  fvline  25153  ellines  25161  filnetlem3  25478  heiborlem6  25688  heiborlem7  25689  heiborlem8  25690  mpt2xopoveq  27259  nbgraop  27373  wlkntrllem2  27462  constr1trl  27484  1pthonlem1  27485  1pthonlem2  27486  1pthon  27487  2trllem1  27490  2pthon  27498  2pthon3v  27500  constr3lem2  27530  bnj97  28409  bnj553  28441  bnj966  28487  bnj1442  28590  dvhvaddval  31098  dvhvscaval  31107  dibglbN  31174  dihglbcpreN  31308  dihmeetlem4preN  31314  dihmeetlem13N  31327  hdmapfval  31838
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683
  Copyright terms: Public domain W3C validator