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

Theorem opex 4923
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 4390 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 prex 4900 . . 3 {{𝐴}, {𝐴, 𝐵}} ∈ V
3 0ex 4781 . . 3 ∅ ∈ V
42, 3ifex 4147 . 2 if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
51, 4eqeltri 2695 1 𝐴, 𝐵⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 1988  Vcvv 3195  c0 3907  ifcif 4077  {csn 4168  {cpr 4170  cop 4174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175
This theorem is referenced by:  otex  4924  otth2  4942  otthg  4944  oteqex2  4953  oteqex  4954  snopeqop  4959  propeqop  4960  propssopi  4961  euop2  4964  opabid  4972  elopab  4973  opabn0  4996  opeliunxp  5160  elvvv  5168  opbrop  5188  relsnop  5214  xpiindi  5246  raliunxp  5250  intirr  5502  xpnz  5541  dmsnn0  5588  dmsnopg  5594  cnvcnvsn  5600  op2ndb  5607  opswap  5610  cnviin  5660  funopg  5910  dffv2  6258  fsn  6387  f1o2sn  6393  funsndifnop  6401  fmptsng  6419  fmptsnd  6420  fvsn  6431  fpr2g  6460  resfunexg  6464  idref  6484  fveqf1o  6542  fliftel  6544  fliftel1  6545  oprabid  6662  dfoprab2  6686  oprabv  6688  rnoprab  6728  eloprabga  6732  ot1stg  7167  ot2ndg  7168  ot3rdg  7169  fo1st  7173  fo2nd  7174  opiota  7214  eloprabi  7217  mpt2sn  7253  fpar  7266  algrflem  7271  frxp  7272  xporderlem  7273  fnwelem  7277  mpt2xopoveq  7330  brtpos  7346  dmtpos  7349  rntpos  7350  tpostpos  7357  wfrlem14  7413  tfrlem11  7469  seqomlem1  7530  seqomlem3  7532  seqomlem4  7533  omeu  7650  iiner  7804  xpsnen  8029  xpcomco  8035  xpassen  8039  xpmapenlem  8112  unxpdomlem1  8149  fseqenlem2  8833  cda1dif  8983  fpwwe  9453  addpipq2  9743  addpqnq  9745  mulpipq2  9746  mulpqnq  9748  ordpipq  9749  prlem934  9840  addcnsr  9941  mulcnsr  9942  ltresr  9946  addcnsrec  9949  mulcnsrec  9950  axcnre  9970  om2uzrdg  12738  uzrdg0i  12741  uzrdgsuci  12742  hashfun  13207  wrdexb  13299  s1len  13368  s1nz  13369  s111  13378  wrdlen2i  13667  brintclab  13723  fsumcnv  14485  fprodcnv  14694  ruclem1  14941  ruclem4  14944  eucalgval2  15275  crth  15464  phimullem  15465  setsval  15869  setsdm  15873  setsfun  15874  setsfun0  15875  setsexstruct2  15878  setsres  15882  setscom  15884  strfv  15888  setsid  15895  imasaddfnlem  16169  imasaddvallem  16170  imasvscafn  16178  idfuval  16517  cofuval  16523  resfval  16533  resfval2  16534  elhoma  16663  embedsetcestrclem  16778  xpcco  16804  xpcid  16810  1stfval  16812  2ndfval  16815  prfval  16820  prf1  16821  prf2  16823  evlfval  16838  curfval  16844  curf1  16846  curfcl  16853  hofval  16873  intopsn  17234  mgm1  17238  sgrp1  17274  mnd1  17312  mnd1id  17313  grpss  17421  grp1  17503  symg2bas  17799  efgmval  18106  efgi  18113  efgi2  18119  frgpnabllem1  18257  frgpnabllem2  18258  ring1  18583  opsrtoslem2  19466  mat1dimelbas  20258  mat1dimbas  20259  mat1dimscm  20262  mat1dimmul  20263  mat1f1o  20265  mat1rhmelval  20267  mvmulfval  20329  m2detleib  20418  txcnp  21404  upxp  21407  uptx  21409  txdis1cn  21419  hauseqlcld  21430  txlm  21432  xkoinjcn  21471  txflf  21791  qustgplem  21905  ucnima  22066  ucnprima  22067  fmucndlem  22076  imasdsf1olem  22159  cnheiborlem  22734  ovollb2lem  23237  ovolctb  23239  ovolshftlem1  23258  ovolscalem1  23262  ovolicc1  23265  ioombl1lem3  23309  ioombl1lem4  23310  ioorval  23323  dyadval  23341  mbfimaopnlem  23403  limccnp2  23637  brbtwn  25760  brcgr  25761  eengbas  25842  ebtwntg  25843  ecgrtg  25844  elntg  25845  structvtxval  25891  structgrssvtx  25894  structgrssiedg  25895  structgrssvtxOLD  25897  structgrssiedgOLD  25898  gropd  25904  isuhgrop  25946  uhgrunop  25951  upgrop  25970  upgr0eop  25990  upgrunop  25995  umgrunop  25997  isuspgrop  26037  isusgrop  26038  ausgrusgrb  26041  usgr0eop  26119  usgrexmpl  26136  griedg0ssusgr  26138  uhgrspanop  26169  uhgrspan1  26176  upgrres  26179  umgrres  26180  usgrres  26181  upgrres1  26186  umgrres1  26187  usgrres1  26188  nbupgruvtxres  26289  usgrexi  26318  cusgrexi  26320  cffldtocusgr  26324  cusgrres  26325  vtxdgop  26347  umgr2v2e  26402  wlkp1lem2  26552  wlkpwwlkf1ouspgr  26746  wlkwwlksur  26764  wwlksnext  26769  eupth2eucrct  27057  eupthvdres  27075  konigsbergumgr  27092  konigsbergupgrOLD  27093  numclwlk1lem2fv  27197  ex-br  27258  cnnvg  27503  cnnvs  27505  cnnvnm  27506  h2hva  27801  h2hsm  27802  h2hnm  27803  hhssva  28084  hhsssm  28085  hhssnm  28086  hhshsslem1  28094  br8d  29394  xppreima2  29423  aciunf1lem  29435  ofpreima  29439  cnvoprab  29472  smatrcl  29836  smatlem  29837  fvproj  29873  fimaproj  29874  txomap  29875  qtophaus  29877  hgt750lemb  30708  bnj97  30910  bnj553  30942  bnj966  30988  bnj1442  31091  erdszelem9  31155  erdszelem10  31156  txpconn  31188  txsconnlem  31196  msubval  31396  mvhval  31405  msubvrs  31431  brtpid1  31577  brtpid2  31578  brtpid3  31579  brtp  31614  dfpo2  31620  br8  31621  br6  31622  br4  31623  br1steq  31646  br2ndeq  31647  dfdm5  31650  dfrn5  31651  elima4  31653  fv1stcnv  31654  fv2ndcnv  31655  brv  31959  brtxp  31962  brpprod  31967  brpprod3b  31969  brsset  31971  brtxpsd  31976  dffun10  31996  elfuns  31997  brcart  32014  brimg  32019  brapply  32020  brcup  32021  brcap  32022  brsuccf  32023  brrestrict  32031  dfrecs2  32032  dfrdg4  32033  fvtransport  32114  brcolinear2  32140  colineardim1  32143  brsegle  32190  fvline  32226  ellines  32234  filnetlem3  32350  bj-inftyexpiinv  33066  bj-inftyexpidisj  33068  bj-elccinfty  33072  bj-minftyccb  33083  finxpreclem2  33198  finxp0  33199  finxp1o  33200  finxpreclem3  33201  finxpreclem4  33202  finxpreclem5  33203  finxpreclem6  33204  poimirlem9  33389  poimirlem15  33395  poimirlem17  33397  poimirlem20  33400  poimirlem24  33404  poimirlem28  33408  mblfinlem2  33418  heiborlem6  33586  heiborlem7  33587  heiborlem8  33588  grposnOLD  33652  rngosn3  33694  gidsn  33722  zrdivrng  33723  dvhvaddval  36198  dvhvscaval  36207  dibglbN  36274  dihglbcpreN  36408  dihmeetlem4preN  36414  dihmeetlem13N  36427  hdmapfval  36938  elcnvlem  37726  cotrintab  37740  elimaint  37759  snhesn  37900  projf1o  39202  dvnprodlem1  39924  dvnprodlem2  39925  sge0xp  40409  hoicvr  40525  hoicvrrex  40533  hoidmv1le  40571  hoi2toco  40584  ovnlecvr2  40587  ovolval5lem2  40630  setsidel  41110  opeliun2xp  41876  lmod1lem2  42042  lmod1lem3  42043  lmod1zr  42047  zlmodzxznm  42051  zlmodzxzldeplem  42052
  Copyright terms: Public domain W3C validator