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

Theorem opex 5353
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 4799 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 prex 5329 . . 3 {{𝐴}, {𝐴, 𝐵}} ∈ V
3 0ex 5208 . . 3 ∅ ∈ V
42, 3ifex 4518 . 2 if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
51, 4eqeltri 2914 1 𝐴, 𝐵⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2107  Vcvv 3500  c0 4295  ifcif 4470  {csn 4564  {cpr 4566  cop 4570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571
This theorem is referenced by:  otex  5354  brv  5361  otth2  5372  otthg  5374  sbcop1  5376  oteqex2  5386  oteqex  5387  snopeqop  5393  propeqop  5394  propssopi  5395  euop2  5399  opabidw  5409  opabid  5410  elopab  5411  rexopabb  5412  opabn0  5437  opeliunxp  5618  elvvv  5626  opbrop  5647  relsnopg  5675  xpiindi  5705  raliunxp  5709  idrefALT  5971  intirr  5976  xpnz  6014  dmsnn0  6062  dmsnopg  6068  cnvcnvsn  6074  op2ndb  6082  opswap  6084  cnviin  6135  reuop  6142  funopg  6386  dffv2  6753  fsn  6893  f1o2sn  6900  idref  6904  funsndifnop  6909  fmptsng  6926  fmptsnd  6927  fvsng  6938  resfunexg  6973  fveqf1o  7052  fliftel  7054  fliftel1  7055  oprabidw  7179  oprabid  7180  dfoprab2  7204  oprabv  7206  rnoprab  7247  eloprabga  7251  ot1stg  7694  ot2ndg  7695  ot3rdg  7696  fo1st  7700  fo2nd  7701  br1steqg  7702  br2ndeqg  7703  opiota  7748  eloprabi  7752  mposn  7789  fpar  7802  fsplitfpar  7805  algrflem  7810  frxp  7811  xporderlem  7812  fnwelem  7816  fvproj  7819  fimaproj  7820  mpoxopoveq  7876  brtpos  7892  dmtpos  7895  rntpos  7896  tpostpos  7903  wfrlem14  7959  tfrlem11  8015  seqomlem1  8077  seqomlem3  8079  seqomlem4  8080  omeu  8201  iiner  8359  xpsnen  8590  xpcomco  8596  xpassen  8600  xpmapenlem  8673  unxpdomlem1  8711  inlresf  9332  inrresf  9334  djur  9337  djuss  9338  djuun  9344  1stinl  9345  2ndinl  9346  1stinr  9347  2ndinr  9348  fseqenlem2  9440  dju1dif  9587  fpwwe  10057  addpipq2  10347  addpqnq  10349  mulpipq2  10350  mulpqnq  10352  ordpipq  10353  prlem934  10444  addcnsr  10546  mulcnsr  10547  ltresr  10551  addcnsrec  10554  mulcnsrec  10555  axcnre  10575  om2uzrdg  13314  uzrdg0i  13317  uzrdgsuci  13318  hashfun  13788  wrdexb  13863  s1len  13950  s1nz  13951  s111  13959  wrdlen2i  14294  brintclab  14351  fsumcnv  15118  fprodcnv  15327  ruclem1  15574  ruclem4  15577  eucalgval2  15915  crth  16105  phimullem  16106  setsval  16503  setsdm  16507  setsfun  16508  setsfun0  16509  setsexstruct2  16512  setsres  16515  setscom  16517  strfv  16521  setsid  16528  imasaddfnlem  16791  imasaddvallem  16792  imasvscafn  16800  idfuval  17136  cofuval  17142  resfval  17152  resfval2  17153  elhoma  17282  embedsetcestrclem  17397  xpcco  17423  xpcid  17429  1stfval  17431  2ndfval  17434  prfval  17439  prf1  17440  prf2  17442  evlfval  17457  curfval  17463  curf1  17465  curfcl  17472  hofval  17492  intopsn  17853  mgm1  17857  sgrp1  17899  mnd1  17940  mnd1id  17941  grpss  18051  grp1  18136  symg2bas  18446  efgmval  18758  efgi  18765  efgi2  18771  frgpnabllem1  18913  frgpnabllem2  18914  ring1  19272  opsrtoslem2  20183  mat1dimelbas  20996  mat1dimbas  20997  mat1dimscm  21000  mat1dimmul  21001  mat1f1o  21003  mat1rhmelval  21005  mvmulfval  21067  m2detleib  21156  txcnp  22144  upxp  22147  uptx  22149  txdis1cn  22159  hauseqlcld  22170  txlm  22172  xkoinjcn  22211  txflf  22530  qustgplem  22644  ucnima  22805  ucnprima  22806  fmucndlem  22815  imasdsf1olem  22898  cnheiborlem  23473  ovollb2lem  24004  ovolctb  24006  ovolshftlem1  24025  ovolscalem1  24029  ovolicc1  24032  ioombl1lem3  24076  ioombl1lem4  24077  ioorval  24090  dyadval  24108  mbfimaopnlem  24171  limccnp2  24405  brbtwn  26599  brcgr  26600  eengbas  26681  ebtwntg  26682  ecgrtg  26683  elntg  26684  structvtxval  26720  structgrssvtx  26723  structgrssiedg  26724  gropd  26730  isuhgrop  26769  uhgrunop  26774  upgrop  26793  upgr0eop  26813  upgrunop  26818  umgrunop  26820  isuspgrop  26860  isusgrop  26861  ausgrusgrb  26864  usgr0eop  26942  usgrexmpl  26959  griedg0ssusgr  26961  uhgrspanop  26992  uhgrspan1  26999  upgrres  27002  umgrres  27003  usgrres  27004  upgrres1  27009  umgrres1  27010  usgrres1  27011  usgrexi  27137  cusgrexi  27139  cffldtocusgr  27143  cusgrres  27144  vtxdgop  27166  umgr2v2e  27221  wlkp1lem2  27370  wlkswwlksf1o  27571  wwlksnext  27585  eupth2eucrct  27910  eupthvdres  27928  konigsbergumgr  27944  numclwwlk1lem2fv  28049  numclwlk1lem1  28062  ex-br  28124  ex-fpar  28155  cnnvg  28369  cnnvs  28371  cnnvnm  28372  h2hva  28665  h2hsm  28666  h2hnm  28667  hhssva  28948  hhsssm  28949  hhssnm  28950  hhshsslem1  28958  br8d  30276  xppreima2  30310  aciunf1lem  30322  ofpreima  30325  brsnop  30342  cnvoprabOLD  30369  linds2eq  30855  smatrcl  30947  smatlem  30948  txomap  30984  qtophaus  30986  hgt750lemb  31813  bnj97  32024  bnj553  32056  bnj966  32102  bnj1442  32205  erdszelem9  32330  erdszelem10  32331  txpconn  32363  txsconnlem  32371  goel  32478  goeleq12bg  32480  gonafv  32481  gonanegoal  32483  sat1el2xp  32510  fmlaomn0  32521  gonan0  32523  goaln0  32524  gonarlem  32525  gonar  32526  goalrlem  32527  goalr  32528  fmla0disjsuc  32529  fmlasucdisj  32530  satffunlem  32532  satffunlem1lem1  32533  satffunlem2lem1  32535  satfv0fvfmla0  32544  sategoelfvb  32550  prv1n  32562  msubval  32656  mvhval  32665  msubvrs  32691  brtpid1  32835  brtpid2  32836  brtpid3  32837  brtp  32869  dfpo2  32875  br8  32876  br6  32877  br4  32878  dfdm5  32900  dfrn5  32901  elima4  32903  fv1stcnv  32904  fv2ndcnv  32905  brtxp  33225  brpprod  33230  brpprod3b  33232  brsset  33234  brtxpsd  33239  dffun10  33259  elfuns  33260  brcart  33277  brimg  33282  brapply  33283  brcup  33284  brcap  33285  brsuccf  33286  brrestrict  33294  dfrecs2  33295  dfrdg4  33296  fvtransport  33377  brcolinear2  33403  colineardim1  33406  brsegle  33453  fvline  33489  ellines  33497  filnetlem3  33612  bj-inftyexpitaufo  34363  bj-inftyexpitaudisj  34366  bj-inftyexpiinv  34369  bj-inftyexpidisj  34371  bj-elccinfty  34375  bj-minftyccb  34386  finxpreclem2  34540  finxp0  34541  finxp1o  34542  finxpreclem3  34543  finxpreclem4  34544  finxpreclem5  34545  finxpreclem6  34546  poimirlem9  34768  poimirlem15  34774  poimirlem17  34776  poimirlem20  34779  poimirlem24  34783  poimirlem28  34787  mblfinlem2  34797  heiborlem6  34962  heiborlem7  34963  heiborlem8  34964  grposnOLD  35028  rngosn3  35070  gidsn  35098  zrdivrng  35099  brxrn  35493  br1cossxrnres  35555  dvhvaddval  38093  dvhvscaval  38102  dibglbN  38169  dihglbcpreN  38303  dihmeetlem4preN  38309  dihmeetlem13N  38322  hdmapfval  38830  elcnvlem  39826  cotrintab  39839  elimaint  39858  snhesn  39997  projf1o  41324  dvnprodlem1  42096  dvnprodlem2  42097  sge0xp  42577  hoicvr  42696  hoicvrrex  42704  hoidmv1le  42742  hoi2toco  42755  ovnlecvr2  42758  ovolval5lem2  42801  setsidel  43402  prproropf1olem3  43499  prproropf1olem4  43500  prproropreud  43503  ushrisomgr  43838  opeliun2xp  44213  lmod1lem2  44375  lmod1lem3  44376  lmod1zr  44380  zlmodzxznm  44384  zlmodzxzldeplem  44385  rrx2xpref1o  44537  line2x  44573  inlinecirc02plem  44605
  Copyright terms: Public domain W3C validator