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

Theorem opex 4849
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 4327 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 prex 4827 . . 3 {{𝐴}, {𝐴, 𝐵}} ∈ V
3 0ex 4709 . . 3 ∅ ∈ V
42, 3ifex 4101 . 2 if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
51, 4eqeltri 2679 1 𝐴, 𝐵⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 382  wcel 1975  Vcvv 3168  c0 3869  ifcif 4031  {csn 4120  {cpr 4122  cop 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127
This theorem is referenced by:  otex  4850  otth2  4868  otthg  4870  oteqex2  4878  oteqex  4879  euop2  4886  opabid  4893  elopab  4894  opabn0  4917  opeliunxp  5079  elvvv  5087  opbrop  5107  relsnop  5132  xpiindi  5163  raliunxp  5167  intirr  5416  xpnz  5454  dmsnn0  5500  dmsnopg  5506  cnvcnvsn  5512  op2ndb  5519  opswap  5522  cnviin  5571  funopg  5818  dffv2  6162  fsn  6289  f1o2sn  6295  fmptsng  6313  fmptsnd  6314  fvsn  6325  fpr2g  6354  resfunexg  6358  idref  6377  fveqf1o  6431  fliftel  6433  fliftel1  6434  oprabid  6550  dfoprab2  6573  oprabv  6575  rnoprab  6615  eloprabga  6619  ot1stg  7046  ot2ndg  7047  ot3rdg  7048  fo1st  7052  fo2nd  7053  opiota  7091  eloprabi  7094  mpt2sn  7128  fpar  7141  algrflem  7146  frxp  7147  xporderlem  7148  fnwelem  7152  mpt2xopoveq  7205  brtpos  7221  dmtpos  7224  rntpos  7225  tpostpos  7232  wfrlem14  7288  tfrlem11  7344  seqomlem1  7405  seqomlem3  7407  seqomlem4  7408  omeu  7525  iiner  7679  xpsnen  7902  xpcomco  7908  xpassen  7912  xpmapenlem  7985  unxpdomlem1  8022  fseqenlem2  8704  cda1dif  8854  fpwwe  9320  addpipq2  9610  addpqnq  9612  mulpipq2  9613  mulpqnq  9615  ordpipq  9616  prlem934  9707  addcnsr  9808  mulcnsr  9809  ltresr  9813  addcnsrec  9816  mulcnsrec  9817  axcnre  9837  om2uzrdg  12568  uzrdg0i  12571  uzrdgsuci  12572  hashfun  13032  wrdexb  13113  s1len  13180  s1nz  13181  s111  13190  wrdlen2i  13476  brintclab  13532  fsumcnv  14288  fprodcnv  14494  ruclem1  14741  ruclem4  14744  eucalgval2  15074  crth  15263  phimullem  15264  setsval  15662  setsdm  15666  setsfun  15667  setsfun0  15668  setsres  15671  setscom  15673  strfv  15677  setsid  15684  imasaddfnlem  15953  imasaddvallem  15954  imasvscafn  15962  idfuval  16301  cofuval  16307  resfval  16317  resfval2  16318  elhoma  16447  embedsetcestrclem  16562  xpcco  16588  xpcid  16594  1stfval  16596  2ndfval  16599  prfval  16604  prf1  16605  prf2  16607  evlfval  16622  curfval  16628  curf1  16630  curfcl  16637  hofval  16657  intopsn  17018  mgm1  17022  sgrp1  17058  mnd1  17096  mnd1id  17097  grpss  17205  grp1  17287  symg2bas  17583  efgmval  17890  efgi  17897  efgi2  17903  frgpnabllem1  18041  frgpnabllem2  18042  ring1  18367  opsrtoslem2  19248  mat1dimelbas  20034  mat1dimbas  20035  mat1dimscm  20038  mat1dimmul  20039  mat1f1o  20041  mat1rhmelval  20043  mvmulfval  20105  m2detleib  20194  txcnp  21171  upxp  21174  uptx  21176  txdis1cn  21186  hauseqlcld  21197  txlm  21199  xkoinjcn  21238  txflf  21558  qustgplem  21672  ucnima  21833  ucnprima  21834  fmucndlem  21843  imasdsf1olem  21925  cnheiborlem  22488  ovollb2lem  22976  ovolctb  22978  ovolshftlem1  22997  ovolscalem1  23001  ovolicc1  23004  ioombl1lem3  23048  ioombl1lem4  23049  ioorval  23061  dyadval  23079  mbfimaopnlem  23141  limccnp2  23375  brbtwn  25493  brcgr  25494  eengbas  25575  ebtwntg  25576  ecgrtg  25577  elntg  25578  edgopval  25631  nbgraop  25714  nbgraopALT  25715  2trllemA  25842  constr1trl  25880  1pthonlem1  25881  1pthonlem2  25882  1pthon  25883  2pthon  25894  2pthon3v  25896  constr3lem2  25936  wlkiswwlksur  26009  wwlknext  26014  el2wlkonotot0  26161  numclwlk1lem2fv  26382  ex-br  26442  cnnvg  26709  cnnvs  26712  cnnvnm  26713  h2hva  27017  h2hsm  27018  h2hnm  27019  hhssva  27300  hhsssm  27301  hhssnm  27302  hhshsslem1  27310  br8d  28604  xppreima2  28632  aciunf1lem  28646  ofpreima  28650  cnvoprab  28688  smatrcl  28992  smatlem  28993  fvproj  29029  fimaproj  29030  txomap  29031  qtophaus  29033  bnj97  29992  bnj553  30024  bnj966  30070  bnj1442  30173  erdszelem9  30237  erdszelem10  30238  txpcon  30270  txsconlem  30278  msubval  30478  mvhval  30487  msubvrs  30513  brtpid1  30659  brtpid2  30660  brtpid3  30661  brtp  30694  dfpo2  30700  br8  30701  br6  30702  br4  30703  br1steq  30719  br2ndeq  30720  dfdm5  30723  dfrn5  30724  elima4  30726  fv1stcnv  30727  fv2ndcnv  30728  brv  30956  brtxp  30959  brpprod  30964  brpprod3b  30966  brsset  30968  brtxpsd  30973  dffun10  30993  elfuns  30994  brcart  31011  brimg  31016  brapply  31017  brcup  31018  brcap  31019  brsuccf  31020  brrestrict  31028  dfrecs2  31029  dfrdg4  31030  fvtransport  31111  brcolinear2  31137  colineardim1  31140  brsegle  31187  fvline  31223  ellines  31231  filnetlem3  31347  bj-inftyexpiinv  32071  bj-inftyexpidisj  32073  bj-elccinfty  32077  bj-minftyccb  32088  finxpreclem2  32202  finxp0  32203  finxp1o  32204  finxpreclem3  32205  finxpreclem4  32206  finxpreclem5  32207  finxpreclem6  32208  poimirlem9  32387  poimirlem15  32393  poimirlem17  32395  poimirlem20  32398  poimirlem24  32402  poimirlem28  32406  mblfinlem2  32416  heiborlem6  32584  heiborlem7  32585  heiborlem8  32586  grposnOLD  32650  rngosn3  32692  gidsn  32720  zrdivrng  32721  dvhvaddval  35196  dvhvscaval  35205  dibglbN  35272  dihglbcpreN  35406  dihmeetlem4preN  35412  dihmeetlem13N  35425  hdmapfval  35936  elcnvlem  36725  cotrintab  36739  elimaint  36758  snhesn  36899  projf1o  38180  dvnprodlem1  38636  dvnprodlem2  38637  sge0xp  39122  hoicvr  39238  hoicvrrex  39246  hoidmv1le  39284  hoi2toco  39297  ovnlecvr2  39300  ovolval5lem2  39343  snopeqop  40121  propeqop  40122  propssopi  40123  funsndifnop  40144  structgrssvtx  40255  structgrssiedg  40256  gropd  40262  vtxvalsnop  40270  iedgvalsnop  40271  isuhgrop  40293  uhgrunop  40298  upgr0eop  40337  edgaopval  40352  isusgrop  40390  ausgrusgrb  40393  usgr0eop  40470  usgrexmpledg  40484  usgrexmpl  40485  griedg0ssusgr  40487  uhgrspanop  40518  uhgrspan1  40525  upgrres1  40530  umgrres1  40531  usgrres1  40532  nbupgrres  40590  nbupgruvtxres  40632  usgrexi  40659  cusgrexi  40660  cusgrres  40662  umgr2v2eedg  40738  umgr2v2e  40739  1wlkp1lem2  40881  1wlkpwwlkf1ouspgr  41074  wlkwwlksur  41092  wwlksnext  41097  ntrl2v2e  41323  eupth2eucrct  41383  eupthvdres  41401  konigsbergumgr  41418  konigsbergupgrOLD  41419  av-numclwlk1lem2fv  41521  opeliun2xp  41902  lmod1lem2  42069  lmod1lem3  42070  lmod1zr  42074  zlmodzxznm  42078  zlmodzxzldeplem  42079
  Copyright terms: Public domain W3C validator