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

Theorem opex 5347
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 4792 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 prex 5323 . . 3 {{𝐴}, {𝐴, 𝐵}} ∈ V
3 0ex 5202 . . 3 ∅ ∈ V
42, 3ifex 4511 . 2 if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
51, 4eqeltri 2906 1 𝐴, 𝐵⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2105  Vcvv 3492  c0 4288  ifcif 4463  {csn 4557  {cpr 4559  cop 4563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564
This theorem is referenced by:  otex  5348  brv  5355  otth2  5366  otthg  5368  sbcop1  5370  oteqex2  5380  oteqex  5381  snopeqop  5387  propeqop  5388  propssopi  5389  euop2  5393  opabidw  5403  opabid  5404  elopab  5405  rexopabb  5406  opabn0  5431  opeliunxp  5612  elvvv  5620  opbrop  5641  relsnopg  5669  xpiindi  5699  raliunxp  5703  idrefALT  5966  intirr  5971  xpnz  6009  dmsnn0  6057  dmsnopg  6063  cnvcnvsn  6069  op2ndb  6077  opswap  6079  cnviin  6130  reuop  6137  funopg  6382  dffv2  6749  fsn  6889  f1o2sn  6896  idref  6900  funsndifnop  6905  fmptsng  6922  fmptsnd  6923  fvsng  6934  resfunexg  6969  fveqf1o  7049  fliftel  7051  fliftel1  7052  oprabidw  7176  oprabid  7177  dfoprab2  7201  oprabv  7203  rnoprab  7246  eloprabga  7250  ot1stg  7692  ot2ndg  7693  ot3rdg  7694  fo1st  7698  fo2nd  7699  br1steqg  7700  br2ndeqg  7701  opiota  7746  eloprabi  7750  mposn  7787  fpar  7800  fsplitfpar  7803  algrflem  7808  frxp  7809  xporderlem  7810  fnwelem  7814  fvproj  7817  fimaproj  7818  mpoxopoveq  7874  brtpos  7890  dmtpos  7893  rntpos  7894  tpostpos  7901  wfrlem14  7957  tfrlem11  8013  seqomlem1  8075  seqomlem3  8077  seqomlem4  8078  omeu  8200  iiner  8358  xpsnen  8589  xpcomco  8595  xpassen  8599  xpmapenlem  8672  unxpdomlem1  8710  inlresf  9331  inrresf  9333  djur  9336  djuss  9337  djuun  9343  1stinl  9344  2ndinl  9345  1stinr  9346  2ndinr  9347  fseqenlem2  9439  dju1dif  9586  fpwwe  10056  addpipq2  10346  addpqnq  10348  mulpipq2  10349  mulpqnq  10351  ordpipq  10352  prlem934  10443  addcnsr  10545  mulcnsr  10546  ltresr  10550  addcnsrec  10553  mulcnsrec  10554  axcnre  10574  om2uzrdg  13312  uzrdg0i  13315  uzrdgsuci  13316  hashfun  13786  wrdexb  13861  s1len  13948  s1nz  13949  s111  13957  wrdlen2i  14292  brintclab  14349  fsumcnv  15116  fprodcnv  15325  ruclem1  15572  ruclem4  15575  eucalgval2  15913  crth  16103  phimullem  16104  setsval  16501  setsdm  16505  setsfun  16506  setsfun0  16507  setsexstruct2  16510  setsres  16513  setscom  16515  strfv  16519  setsid  16526  imasaddfnlem  16789  imasaddvallem  16790  imasvscafn  16798  idfuval  17134  cofuval  17140  resfval  17150  resfval2  17151  elhoma  17280  embedsetcestrclem  17395  xpcco  17421  xpcid  17427  1stfval  17429  2ndfval  17432  prfval  17437  prf1  17438  prf2  17440  evlfval  17455  curfval  17461  curf1  17463  curfcl  17470  hofval  17490  intopsn  17852  mgm1  17856  sgrp1  17898  mnd1  17940  mnd1id  17941  grpss  18059  grp1  18144  symg2bas  18455  efgmval  18767  efgi  18774  efgi2  18780  frgpnabllem1  18922  frgpnabllem2  18923  ring1  19281  opsrtoslem2  20193  mat1dimelbas  21008  mat1dimbas  21009  mat1dimscm  21012  mat1dimmul  21013  mat1f1o  21015  mat1rhmelval  21017  mvmulfval  21079  m2detleib  21168  txcnp  22156  upxp  22159  uptx  22161  txdis1cn  22171  hauseqlcld  22182  txlm  22184  xkoinjcn  22223  txflf  22542  qustgplem  22656  ucnima  22817  ucnprima  22818  fmucndlem  22827  imasdsf1olem  22910  cnheiborlem  23485  ovollb2lem  24016  ovolctb  24018  ovolshftlem1  24037  ovolscalem1  24041  ovolicc1  24044  ioombl1lem3  24088  ioombl1lem4  24089  ioorval  24102  dyadval  24120  mbfimaopnlem  24183  limccnp2  24417  brbtwn  26612  brcgr  26613  eengbas  26694  ebtwntg  26695  ecgrtg  26696  elntg  26697  structvtxval  26733  structgrssvtx  26736  structgrssiedg  26737  gropd  26743  isuhgrop  26782  uhgrunop  26787  upgrop  26806  upgr0eop  26826  upgrunop  26831  umgrunop  26833  isuspgrop  26873  isusgrop  26874  ausgrusgrb  26877  usgr0eop  26955  usgrexmpl  26972  griedg0ssusgr  26974  uhgrspanop  27005  uhgrspan1  27012  upgrres  27015  umgrres  27016  usgrres  27017  upgrres1  27022  umgrres1  27023  usgrres1  27024  usgrexi  27150  cusgrexi  27152  cffldtocusgr  27156  cusgrres  27157  vtxdgop  27179  umgr2v2e  27234  wlkp1lem2  27383  wlkswwlksf1o  27584  wwlksnext  27598  eupth2eucrct  27923  eupthvdres  27941  konigsbergumgr  27957  numclwwlk1lem2fv  28062  numclwlk1lem1  28075  ex-br  28137  ex-fpar  28168  cnnvg  28382  cnnvs  28384  cnnvnm  28385  h2hva  28678  h2hsm  28679  h2hnm  28680  hhssva  28961  hhsssm  28962  hhssnm  28963  hhshsslem1  28971  br8d  30289  xppreima2  30323  aciunf1lem  30335  ofpreima  30338  brsnop  30355  cnvoprabOLD  30382  linds2eq  30868  smatrcl  30960  smatlem  30961  txomap  30997  qtophaus  30999  hgt750lemb  31826  bnj97  32037  bnj553  32069  bnj966  32115  bnj1442  32218  erdszelem9  32343  erdszelem10  32344  txpconn  32376  txsconnlem  32384  goel  32491  goeleq12bg  32493  gonafv  32494  gonanegoal  32496  sat1el2xp  32523  fmlaomn0  32534  gonan0  32536  goaln0  32537  gonarlem  32538  gonar  32539  goalrlem  32540  goalr  32541  fmla0disjsuc  32542  fmlasucdisj  32543  satffunlem  32545  satffunlem1lem1  32546  satffunlem2lem1  32548  satfv0fvfmla0  32557  sategoelfvb  32563  prv1n  32575  msubval  32669  mvhval  32678  msubvrs  32704  brtpid1  32848  brtpid2  32849  brtpid3  32850  brtp  32882  dfpo2  32888  br8  32889  br6  32890  br4  32891  dfdm5  32913  dfrn5  32914  elima4  32916  fv1stcnv  32917  fv2ndcnv  32918  brtxp  33238  brpprod  33243  brpprod3b  33245  brsset  33247  brtxpsd  33252  dffun10  33272  elfuns  33273  brcart  33290  brimg  33295  brapply  33296  brcup  33297  brcap  33298  brsuccf  33299  brrestrict  33307  dfrecs2  33308  dfrdg4  33309  fvtransport  33390  brcolinear2  33416  colineardim1  33419  brsegle  33466  fvline  33502  ellines  33510  filnetlem3  33625  bj-inftyexpitaufo  34376  bj-inftyexpitaudisj  34379  bj-inftyexpiinv  34382  bj-inftyexpidisj  34384  bj-elccinfty  34388  bj-minftyccb  34399  finxpreclem2  34553  finxp0  34554  finxp1o  34555  finxpreclem3  34556  finxpreclem4  34557  finxpreclem5  34558  finxpreclem6  34559  poimirlem9  34782  poimirlem15  34788  poimirlem17  34790  poimirlem20  34793  poimirlem24  34797  poimirlem28  34801  mblfinlem2  34811  heiborlem6  34975  heiborlem7  34976  heiborlem8  34977  grposnOLD  35041  rngosn3  35083  gidsn  35111  zrdivrng  35112  brxrn  35506  br1cossxrnres  35568  dvhvaddval  38106  dvhvscaval  38115  dibglbN  38182  dihglbcpreN  38316  dihmeetlem4preN  38322  dihmeetlem13N  38335  hdmapfval  38843  elcnvlem  39839  cotrintab  39852  elimaint  39871  snhesn  40010  projf1o  41335  dvnprodlem1  42107  dvnprodlem2  42108  sge0xp  42588  hoicvr  42707  hoicvrrex  42715  hoidmv1le  42753  hoi2toco  42766  ovnlecvr2  42769  ovolval5lem2  42812  setsidel  43413  prproropf1olem3  43544  prproropf1olem4  43545  prproropreud  43548  ushrisomgr  43883  opeliun2xp  44309  lmod1lem2  44471  lmod1lem3  44472  lmod1zr  44476  zlmodzxznm  44480  zlmodzxzldeplem  44481  rrx2xpref1o  44633  line2x  44669  inlinecirc02plem  44701
  Copyright terms: Public domain W3C validator