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

Theorem opex 4859
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 4337 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 prex 4836 . . 3 {{𝐴}, {𝐴, 𝐵}} ∈ V
3 0ex 4718 . . 3 ∅ ∈ V
42, 3ifex 4106 . 2 if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
51, 4eqeltri 2684 1 𝐴, 𝐵⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 383  wcel 1977  Vcvv 3173  c0 3874  ifcif 4036  {csn 4125  {cpr 4127  cop 4131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132
This theorem is referenced by:  otex  4860  otth2  4878  otthg  4880  oteqex2  4888  oteqex  4889  snopeqop  4894  propeqop  4895  propssopi  4896  euop2  4899  opabid  4907  elopab  4908  opabn0  4931  opeliunxp  5093  elvvv  5101  opbrop  5121  relsnop  5147  xpiindi  5179  raliunxp  5183  intirr  5433  xpnz  5472  dmsnn0  5518  dmsnopg  5524  cnvcnvsn  5530  op2ndb  5537  opswap  5540  cnviin  5589  funopg  5836  dffv2  6181  fsn  6308  f1o2sn  6314  funsndifnop  6321  fmptsng  6339  fmptsnd  6340  fvsn  6351  fpr2g  6380  resfunexg  6384  idref  6403  fveqf1o  6457  fliftel  6459  fliftel1  6460  oprabid  6576  dfoprab2  6599  oprabv  6601  rnoprab  6641  eloprabga  6645  ot1stg  7073  ot2ndg  7074  ot3rdg  7075  fo1st  7079  fo2nd  7080  opiota  7118  eloprabi  7121  mpt2sn  7155  fpar  7168  algrflem  7173  frxp  7174  xporderlem  7175  fnwelem  7179  mpt2xopoveq  7232  brtpos  7248  dmtpos  7251  rntpos  7252  tpostpos  7259  wfrlem14  7315  tfrlem11  7371  seqomlem1  7432  seqomlem3  7434  seqomlem4  7435  omeu  7552  iiner  7706  xpsnen  7929  xpcomco  7935  xpassen  7939  xpmapenlem  8012  unxpdomlem1  8049  fseqenlem2  8731  cda1dif  8881  fpwwe  9347  addpipq2  9637  addpqnq  9639  mulpipq2  9640  mulpqnq  9642  ordpipq  9643  prlem934  9734  addcnsr  9835  mulcnsr  9836  ltresr  9840  addcnsrec  9843  mulcnsrec  9844  axcnre  9864  om2uzrdg  12617  uzrdg0i  12620  uzrdgsuci  12621  hashfun  13084  wrdexb  13171  s1len  13238  s1nz  13239  s111  13248  wrdlen2i  13534  brintclab  13590  fsumcnv  14346  fprodcnv  14552  ruclem1  14799  ruclem4  14802  eucalgval2  15132  crth  15321  phimullem  15322  setsval  15720  setsdm  15724  setsfun  15725  setsfun0  15726  setsres  15729  setscom  15731  strfv  15735  setsid  15742  imasaddfnlem  16011  imasaddvallem  16012  imasvscafn  16020  idfuval  16359  cofuval  16365  resfval  16375  resfval2  16376  elhoma  16505  embedsetcestrclem  16620  xpcco  16646  xpcid  16652  1stfval  16654  2ndfval  16657  prfval  16662  prf1  16663  prf2  16665  evlfval  16680  curfval  16686  curf1  16688  curfcl  16695  hofval  16715  intopsn  17076  mgm1  17080  sgrp1  17116  mnd1  17154  mnd1id  17155  grpss  17263  grp1  17345  symg2bas  17641  efgmval  17948  efgi  17955  efgi2  17961  frgpnabllem1  18099  frgpnabllem2  18100  ring1  18425  opsrtoslem2  19306  mat1dimelbas  20096  mat1dimbas  20097  mat1dimscm  20100  mat1dimmul  20101  mat1f1o  20103  mat1rhmelval  20105  mvmulfval  20167  m2detleib  20256  txcnp  21233  upxp  21236  uptx  21238  txdis1cn  21248  hauseqlcld  21259  txlm  21261  xkoinjcn  21300  txflf  21620  qustgplem  21734  ucnima  21895  ucnprima  21896  fmucndlem  21905  imasdsf1olem  21988  cnheiborlem  22561  ovollb2lem  23063  ovolctb  23065  ovolshftlem1  23084  ovolscalem1  23088  ovolicc1  23091  ioombl1lem3  23135  ioombl1lem4  23136  ioorval  23148  dyadval  23166  mbfimaopnlem  23228  limccnp2  23462  brbtwn  25579  brcgr  25580  eengbas  25661  ebtwntg  25662  ecgrtg  25663  elntg  25664  structgrssvtx  25701  structgrssiedg  25702  gropd  25708  vtxvalsnop  25716  iedgvalsnop  25717  isuhgrop  25736  uhgrunop  25741  upgr0eop  25780  upgrunop  25785  umgrunop  25787  edgaopval  25795  edgopval  25869  nbgraop  25952  nbgraopALT  25953  2trllemA  26080  constr1trl  26118  1pthonlem1  26119  1pthonlem2  26120  1pthon  26121  2pthon  26132  2pthon3v  26134  constr3lem2  26174  wlkiswwlksur  26247  wwlknext  26252  el2wlkonotot0  26399  numclwlk1lem2fv  26620  ex-br  26680  cnnvg  26917  cnnvs  26919  cnnvnm  26920  h2hva  27215  h2hsm  27216  h2hnm  27217  hhssva  27498  hhsssm  27499  hhssnm  27500  hhshsslem1  27508  br8d  28802  xppreima2  28830  aciunf1lem  28844  ofpreima  28848  cnvoprab  28886  smatrcl  29190  smatlem  29191  fvproj  29227  fimaproj  29228  txomap  29229  qtophaus  29231  bnj97  30190  bnj553  30222  bnj966  30268  bnj1442  30371  erdszelem9  30435  erdszelem10  30436  txpcon  30468  txsconlem  30476  msubval  30676  mvhval  30685  msubvrs  30711  brtpid1  30857  brtpid2  30858  brtpid3  30859  brtp  30892  dfpo2  30898  br8  30899  br6  30900  br4  30901  br1steq  30917  br2ndeq  30918  dfdm5  30921  dfrn5  30922  elima4  30924  fv1stcnv  30925  fv2ndcnv  30926  brv  31154  brtxp  31157  brpprod  31162  brpprod3b  31164  brsset  31166  brtxpsd  31171  dffun10  31191  elfuns  31192  brcart  31209  brimg  31214  brapply  31215  brcup  31216  brcap  31217  brsuccf  31218  brrestrict  31226  dfrecs2  31227  dfrdg4  31228  fvtransport  31309  brcolinear2  31335  colineardim1  31338  brsegle  31385  fvline  31421  ellines  31429  filnetlem3  31545  bj-inftyexpiinv  32272  bj-inftyexpidisj  32274  bj-elccinfty  32278  bj-minftyccb  32289  finxpreclem2  32403  finxp0  32404  finxp1o  32405  finxpreclem3  32406  finxpreclem4  32407  finxpreclem5  32408  finxpreclem6  32409  poimirlem9  32588  poimirlem15  32594  poimirlem17  32596  poimirlem20  32599  poimirlem24  32603  poimirlem28  32607  mblfinlem2  32617  heiborlem6  32785  heiborlem7  32786  heiborlem8  32787  grposnOLD  32851  rngosn3  32893  gidsn  32921  zrdivrng  32922  dvhvaddval  35397  dvhvscaval  35406  dibglbN  35473  dihglbcpreN  35607  dihmeetlem4preN  35613  dihmeetlem13N  35626  hdmapfval  36137  elcnvlem  36926  cotrintab  36940  elimaint  36959  snhesn  37100  projf1o  38381  dvnprodlem1  38836  dvnprodlem2  38837  sge0xp  39322  hoicvr  39438  hoicvrrex  39446  hoidmv1le  39484  hoi2toco  39497  ovnlecvr2  39500  ovolval5lem2  39543  isusgrop  40392  ausgrusgrb  40395  usgr0eop  40472  usgrexmpledg  40486  usgrexmpl  40487  griedg0ssusgr  40489  uhgrspanop  40520  uhgrspan1  40527  upgrres1  40532  umgrres1  40533  usgrres1  40534  nbupgrres  40592  nbupgruvtxres  40634  usgrexi  40661  cusgrexi  40662  cusgrres  40664  umgr2v2eedg  40740  umgr2v2e  40741  1wlkp1lem2  40883  1wlkpwwlkf1ouspgr  41076  wlkwwlksur  41094  wwlksnext  41099  ntrl2v2e  41325  eupth2eucrct  41385  eupthvdres  41403  konigsbergumgr  41420  konigsbergupgrOLD  41421  av-numclwlk1lem2fv  41523  opeliun2xp  41904  lmod1lem2  42071  lmod1lem3  42072  lmod1zr  42076  zlmodzxznm  42080  zlmodzxzldeplem  42081
  Copyright terms: Public domain W3C validator