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

Theorem opex 5373
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 𝐴, 𝐵⟩ ∈ V

Proof of Theorem opex
StepHypRef Expression
1 dfopif 4797 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 prex 5350 . . 3 {{𝐴}, {𝐴, 𝐵}} ∈ V
3 0ex 5226 . . 3 ∅ ∈ V
42, 3ifex 4506 . 2 if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
51, 4eqeltri 2835 1 𝐴, 𝐵⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 395  wcel 2108  Vcvv 3422  c0 4253  ifcif 4456  {csn 4558  {cpr 4560  cop 4564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565
This theorem is referenced by:  otex  5374  brv  5381  otth2  5392  otthg  5394  sbcop1  5396  oteqex2  5407  oteqex  5408  snopeqop  5414  propeqop  5415  propssopi  5416  euop2  5420  brsnop  5430  opabidw  5431  opabid  5432  elopab  5433  rexopabb  5434  opabn0  5459  opeliunxp  5645  elvvv  5653  opbrop  5674  relsnopg  5702  xpiindi  5733  raliunxp  5737  idrefALT  6007  intirr  6012  xpnz  6051  dmsnn0  6099  dmsnopg  6105  cnvcnvsn  6111  op2ndb  6119  opswap  6121  cnviin  6178  reuop  6185  dfpo2  6188  funopg  6452  dffv2  6845  fsn  6989  f1o2sn  6996  idref  7000  funsndifnop  7005  fmptsng  7022  fmptsnd  7023  fvsng  7034  resfunexg  7073  fveqf1o  7155  fliftel  7160  fliftel1  7161  oprabidw  7286  oprabid  7287  dfoprab2  7311  oprabv  7313  rnoprab  7356  eloprabga  7360  eloprabgaOLD  7361  ot1stg  7818  ot2ndg  7819  ot3rdg  7820  fo1st  7824  fo2nd  7825  br1steqg  7826  br2ndeqg  7827  opiota  7872  eloprabi  7876  mposn  7914  fpar  7927  fsplitfpar  7930  opco1  7935  opco2  7936  frxp  7938  xporderlem  7939  fnwelem  7943  fvproj  7946  fimaproj  7947  mpoxopoveq  8006  brtpos  8022  dmtpos  8025  rntpos  8026  tpostpos  8033  wfrlem14OLD  8124  tfrlem11  8190  seqomlem1  8251  seqomlem3  8253  seqomlem4  8254  omeu  8378  iiner  8536  xpsnen  8796  xpcomco  8802  xpassen  8806  xpmapenlem  8880  dif1en  8907  unxpdomlem1  8956  inlresf  9603  inrresf  9605  djur  9608  djuss  9609  djuun  9615  1stinl  9616  2ndinl  9617  1stinr  9618  2ndinr  9619  fseqenlem2  9712  dju1dif  9859  fpwwe  10333  addpipq2  10623  addpqnq  10625  mulpipq2  10626  mulpqnq  10628  ordpipq  10629  prlem934  10720  addcnsr  10822  mulcnsr  10823  ltresr  10827  addcnsrec  10830  mulcnsrec  10831  axcnre  10851  om2uzrdg  13604  uzrdg0i  13607  uzrdgsuci  13608  hashfun  14080  wrdexb  14156  s1len  14239  s1nz  14240  s111  14248  wrdlen2i  14583  brintclab  14640  fsumcnv  15413  fprodcnv  15621  ruclem1  15868  ruclem4  15871  eucalgval2  16214  crth  16407  phimullem  16408  setsval  16796  setsdm  16799  setsfun  16800  setsfun0  16801  setsexstruct2  16804  setsres  16807  setscom  16809  strfv  16833  setsid  16837  imasaddfnlem  17156  imasaddvallem  17157  imasvscafn  17165  idfuval  17507  cofuval  17513  resfval  17523  resfval2  17524  elhoma  17663  embedsetcestrclem  17790  xpcco  17816  xpcid  17822  1stfval  17824  2ndfval  17827  prfval  17832  prf1  17833  prf2  17835  evlfval  17851  curfval  17857  curf1  17859  curfcl  17866  hofval  17886  intopsn  18253  mgm1  18257  sgrp1  18299  mnd1  18341  mnd1id  18342  grpss  18512  grp1  18597  symg2bas  18915  efgmval  19233  efgi  19240  efgi2  19246  frgpnabllem1  19389  frgpnabllem2  19390  ring1  19756  opsrtoslem2  21173  mat1dimelbas  21528  mat1dimbas  21529  mat1dimscm  21532  mat1dimmul  21533  mat1f1o  21535  mat1rhmelval  21537  mvmulfval  21599  m2detleib  21688  txcnp  22679  upxp  22682  uptx  22684  txdis1cn  22694  hauseqlcld  22705  txlm  22707  xkoinjcn  22746  txflf  23065  qustgplem  23180  ucnima  23341  ucnprima  23342  fmucndlem  23351  imasdsf1olem  23434  cnheiborlem  24023  ovollb2lem  24557  ovolctb  24559  ovolshftlem1  24578  ovolscalem1  24582  ovolicc1  24585  ioombl1lem3  24629  ioombl1lem4  24630  ioorval  24643  dyadval  24661  mbfimaopnlem  24724  limccnp2  24961  brbtwn  27170  brcgr  27171  eengbas  27252  ebtwntg  27253  ecgrtg  27254  elntg  27255  structvtxval  27294  structgrssvtx  27297  structgrssiedg  27298  gropd  27304  isuhgrop  27343  uhgrunop  27348  upgrop  27367  upgr0eop  27387  upgrunop  27392  umgrunop  27394  isuspgrop  27434  isusgrop  27435  ausgrusgrb  27438  usgr0eop  27516  usgrexmpl  27533  griedg0ssusgr  27535  uhgrspanop  27566  uhgrspan1  27573  upgrres  27576  umgrres  27577  usgrres  27578  upgrres1  27583  umgrres1  27584  usgrres1  27585  usgrexi  27711  cusgrexi  27713  cffldtocusgr  27717  cusgrres  27718  vtxdgop  27740  umgr2v2e  27795  wlkp1lem2  27944  wlkswwlksf1o  28145  wwlksnext  28159  eupth2eucrct  28482  eupthvdres  28500  konigsbergumgr  28516  numclwwlk1lem2fv  28621  numclwlk1lem1  28634  ex-br  28696  ex-fpar  28727  cnnvg  28941  cnnvs  28943  cnnvnm  28944  h2hva  29237  h2hsm  29238  h2hnm  29239  hhssva  29520  hhsssm  29521  hhssnm  29522  hhshsslem1  29530  br8d  30851  xppreima2  30889  aciunf1lem  30901  ofpreima  30904  cnvoprabOLD  30957  linds2eq  31477  smatrcl  31648  smatlem  31649  txomap  31686  qtophaus  31688  hgt750lemb  32536  bnj97  32746  bnj553  32778  bnj966  32824  bnj1442  32929  erdszelem9  33061  erdszelem10  33062  txpconn  33094  txsconnlem  33102  goel  33209  goeleq12bg  33211  gonafv  33212  gonanegoal  33214  sat1el2xp  33241  fmlaomn0  33252  gonan0  33254  goaln0  33255  gonarlem  33256  gonar  33257  goalrlem  33258  goalr  33259  fmla0disjsuc  33260  fmlasucdisj  33261  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  satfv0fvfmla0  33275  sategoelfvb  33281  prv1n  33293  msubval  33387  mvhval  33396  msubvrs  33422  brtpid1  33567  brtpid2  33568  brtpid3  33569  ot21std  33583  ot22ndd  33584  otthne  33585  ralxp3f  33588  sbcoteq1a  33590  brtp  33623  br8  33629  br6  33630  br4  33631  dfdm5  33653  dfrn5  33654  elima4  33656  fv1stcnv  33657  fv2ndcnv  33658  xpord2lem  33716  xpord2pred  33719  xpord2ind  33721  xpord3lem  33722  frxp3  33724  xpord3pred  33725  naddcllem  33758  addsval  34053  brtxp  34109  brpprod  34114  brpprod3b  34116  brsset  34118  brtxpsd  34123  dffun10  34143  elfuns  34144  brcart  34161  brimg  34166  brapply  34167  brcup  34168  brcap  34169  brsuccf  34170  brrestrict  34178  dfrecs2  34179  dfrdg4  34180  fvtransport  34261  brcolinear2  34287  colineardim1  34290  brsegle  34337  fvline  34373  ellines  34381  filnetlem3  34496  bj-inftyexpitaufo  35300  bj-inftyexpitaudisj  35303  bj-inftyexpiinv  35306  bj-inftyexpidisj  35308  bj-elccinfty  35312  bj-minftyccb  35323  finxpreclem2  35488  finxp0  35489  finxp1o  35490  finxpreclem3  35491  finxpreclem4  35492  finxpreclem5  35493  finxpreclem6  35494  poimirlem9  35713  poimirlem15  35719  poimirlem17  35721  poimirlem20  35724  poimirlem24  35728  poimirlem28  35732  mblfinlem2  35742  heiborlem6  35901  heiborlem7  35902  heiborlem8  35903  grposnOLD  35967  rngosn3  36009  gidsn  36037  zrdivrng  36038  brxrn  36431  br1cossxrnres  36493  dvhvaddval  39031  dvhvscaval  39040  dibglbN  39107  dihglbcpreN  39241  dihmeetlem4preN  39247  dihmeetlem13N  39260  hdmapfval  39768  elcnvlem  41098  cotrintab  41111  elimaint  41146  snhesn  41283  projf1o  42625  dvnprodlem1  43377  dvnprodlem2  43378  sge0xp  43857  hoicvr  43976  hoicvrrex  43984  hoidmv1le  44022  hoi2toco  44035  ovnlecvr2  44038  ovolval5lem2  44081  fsetsnf1  44433  setsidel  44716  prproropf1olem3  44845  prproropf1olem4  44846  prproropreud  44849  ushrisomgr  45181  opeliun2xp  45556  lmod1lem2  45717  lmod1lem3  45718  lmod1zr  45722  zlmodzxznm  45726  zlmodzxzldeplem  45727  rrx2xpref1o  45952  line2x  45988  inlinecirc02plem  46020  thincciso  46218  mndtchom  46257
  Copyright terms: Public domain W3C validator