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

Theorem opex 5422
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 4828 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 prex 5390 . . 3 {{𝐴}, {𝐴, 𝐵}} ∈ V
3 0ex 5265 . . 3 ∅ ∈ V
42, 3ifex 4537 . 2 if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
51, 4eqeltri 2830 1 𝐴, 𝐵⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 397  wcel 2107  Vcvv 3444  c0 4283  ifcif 4487  {csn 4587  {cpr 4589  cop 4593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594
This theorem is referenced by:  otex  5423  brv  5430  otth2  5441  otthg  5443  sbcop1  5446  oteqex2  5457  oteqex  5458  snopeqop  5464  propeqop  5465  propssopi  5466  euop2  5470  brsnop  5480  brtp  5481  opabidw  5482  opabid  5483  elopab  5485  rexopabb  5486  opabn0  5511  opeliunxp  5700  elvvv  5708  opbrop  5730  relsnopg  5760  xpiindi  5792  raliunxp  5796  idrefALT  6066  intirr  6073  xpnz  6112  dmsnn0  6160  dmsnopg  6166  cnvcnvsn  6172  op2ndb  6180  opswap  6182  cnviin  6239  reuop  6246  dfpo2  6249  funopg  6536  dffv2  6937  fsn  7082  f1o2sn  7089  idref  7093  funsndifnop  7098  fmptsng  7115  fmptsnd  7116  fvsng  7127  resfunexg  7166  fveqf1o  7250  fliftel  7255  fliftel1  7256  oprabidw  7389  oprabid  7390  dfoprab2  7416  oprabv  7418  rnoprab  7461  eloprabga  7465  eloprabgaOLD  7466  ot1stg  7936  ot2ndg  7937  ot3rdg  7938  fo1st  7942  fo2nd  7943  br1steqg  7944  br2ndeqg  7945  opiota  7992  eloprabi  7996  mposn  8036  fpar  8049  fsplitfpar  8051  opco1  8056  opco2  8057  frxp  8059  xporderlem  8060  fnwelem  8064  fvproj  8067  fimaproj  8068  xpord2lem  8075  xpord2pred  8078  xpord2indlem  8080  frxp3  8084  mpoxopoveq  8151  brtpos  8167  dmtpos  8170  rntpos  8171  tpostpos  8178  wfrlem14OLD  8269  tfrlem11  8335  seqomlem1  8397  seqomlem3  8399  seqomlem4  8400  omeu  8533  naddcllem  8623  iiner  8731  xpsnen  9002  xpcomco  9009  xpassen  9013  xpmapenlem  9091  dif1en  9107  dif1enOLD  9109  unxpdomlem1  9197  inlresf  9855  inrresf  9857  djur  9860  djuss  9861  djuun  9867  1stinl  9868  2ndinl  9869  1stinr  9870  2ndinr  9871  fseqenlem2  9966  dju1dif  10113  fpwwe  10587  addpipq2  10877  addpqnq  10879  mulpipq2  10880  mulpqnq  10882  ordpipq  10883  prlem934  10974  addcnsr  11076  mulcnsr  11077  ltresr  11081  addcnsrec  11084  mulcnsrec  11085  axcnre  11105  om2uzrdg  13867  uzrdg0i  13870  uzrdgsuci  13871  hashfun  14343  wrdexb  14419  s1len  14500  s1nz  14501  s111  14509  wrdlen2i  14837  brintclab  14892  fsumcnv  15663  fprodcnv  15871  ruclem1  16118  ruclem4  16121  eucalgval2  16462  crth  16655  phimullem  16656  setsval  17044  setsdm  17047  setsfun  17048  setsfun0  17049  setsexstruct2  17052  setsres  17055  setscom  17057  strfv  17081  setsid  17085  imasaddfnlem  17415  imasaddvallem  17416  imasvscafn  17424  idfuval  17767  cofuval  17773  resfval  17783  resfval2  17784  elhoma  17923  embedsetcestrclem  18050  xpcco  18076  xpcid  18082  1stfval  18084  2ndfval  18087  prfval  18092  prf1  18093  prf2  18095  evlfval  18111  curfval  18117  curf1  18119  curfcl  18126  hofval  18146  intopsn  18514  mgm1  18518  sgrp1  18560  mnd1  18602  mnd1id  18603  grpss  18773  grp1  18859  symg2bas  19179  efgmval  19499  efgi  19506  efgi2  19512  frgpnabllem1  19656  frgpnabllem2  19657  ring1  20031  opsrtoslem2  21479  mat1dimelbas  21836  mat1dimbas  21837  mat1dimscm  21840  mat1dimmul  21841  mat1f1o  21843  mat1rhmelval  21845  mvmulfval  21907  m2detleib  21996  txcnp  22987  upxp  22990  uptx  22992  txdis1cn  23002  hauseqlcld  23013  txlm  23015  xkoinjcn  23054  txflf  23373  qustgplem  23488  ucnima  23649  ucnprima  23650  fmucndlem  23659  imasdsf1olem  23742  cnheiborlem  24333  ovollb2lem  24868  ovolctb  24870  ovolshftlem1  24889  ovolscalem1  24893  ovolicc1  24896  ioombl1lem3  24940  ioombl1lem4  24941  ioorval  24954  dyadval  24972  mbfimaopnlem  25035  limccnp2  25272  addsval  27296  mulsval  27396  brbtwn  27890  brcgr  27891  eengbas  27972  ebtwntg  27973  ecgrtg  27974  elntg  27975  structvtxval  28014  structgrssvtx  28017  structgrssiedg  28018  gropd  28024  isuhgrop  28063  uhgrunop  28068  upgrop  28087  upgr0eop  28107  upgrunop  28112  umgrunop  28114  isuspgrop  28154  isusgrop  28155  ausgrusgrb  28158  usgr0eop  28236  usgrexmpl  28253  griedg0ssusgr  28255  uhgrspanop  28286  uhgrspan1  28293  upgrres  28296  umgrres  28297  usgrres  28298  upgrres1  28303  umgrres1  28304  usgrres1  28305  usgrexi  28431  cusgrexi  28433  cffldtocusgr  28437  cusgrres  28438  vtxdgop  28460  umgr2v2e  28515  wlkp1lem2  28664  wlkswwlksf1o  28866  wwlksnext  28880  eupth2eucrct  29203  eupthvdres  29221  konigsbergumgr  29237  numclwwlk1lem2fv  29342  numclwlk1lem1  29355  ex-br  29417  ex-fpar  29448  cnnvg  29662  cnnvs  29664  cnnvnm  29665  h2hva  29958  h2hsm  29959  h2hnm  29960  hhssva  30241  hhsssm  30242  hhssnm  30243  hhshsslem1  30251  br8d  31575  xppreima2  31613  aciunf1lem  31624  ofpreima  31627  cnvoprabOLD  31684  linds2eq  32216  smatrcl  32434  smatlem  32435  txomap  32472  qtophaus  32474  hgt750lemb  33326  bnj97  33535  bnj553  33567  bnj966  33613  bnj1442  33718  erdszelem9  33850  erdszelem10  33851  txpconn  33883  txsconnlem  33891  goel  33998  goeleq12bg  34000  gonafv  34001  gonanegoal  34003  sat1el2xp  34030  fmlaomn0  34041  gonan0  34043  goaln0  34044  gonarlem  34045  gonar  34046  goalrlem  34047  goalr  34048  fmla0disjsuc  34049  fmlasucdisj  34050  satffunlem  34052  satffunlem1lem1  34053  satffunlem2lem1  34055  satfv0fvfmla0  34064  sategoelfvb  34070  prv1n  34082  msubval  34176  mvhval  34185  msubvrs  34211  brtpid1  34349  brtpid2  34350  brtpid3  34351  br8  34385  br6  34386  br4  34387  dfdm5  34403  dfrn5  34404  elima4  34406  fv1stcnv  34407  fv2ndcnv  34408  brtxp  34511  brpprod  34516  brpprod3b  34518  brsset  34520  brtxpsd  34525  dffun10  34545  elfuns  34546  brcart  34563  brimg  34568  brapply  34569  brcup  34570  brcap  34571  brsuccf  34572  brrestrict  34580  dfrecs2  34581  dfrdg4  34582  fvtransport  34663  brcolinear2  34689  colineardim1  34692  brsegle  34739  fvline  34775  ellines  34783  filnetlem3  34898  bj-inftyexpitaufo  35719  bj-inftyexpitaudisj  35722  bj-inftyexpiinv  35725  bj-inftyexpidisj  35727  bj-elccinfty  35731  bj-minftyccb  35742  finxpreclem2  35907  finxp0  35908  finxp1o  35909  finxpreclem3  35910  finxpreclem4  35911  finxpreclem5  35912  finxpreclem6  35913  poimirlem9  36133  poimirlem15  36139  poimirlem17  36141  poimirlem20  36144  poimirlem24  36148  poimirlem28  36152  mblfinlem2  36162  heiborlem6  36321  heiborlem7  36322  heiborlem8  36323  grposnOLD  36387  rngosn3  36429  gidsn  36457  zrdivrng  36458  brxrn  36882  br1cossxrnres  36956  dvhvaddval  39599  dvhvscaval  39608  dibglbN  39675  dihglbcpreN  39809  dihmeetlem4preN  39815  dihmeetlem13N  39828  hdmapfval  40336  elcnvlem  41961  cotrintab  41974  elimaint  42009  snhesn  42146  projf1o  43505  dvnprodlem1  44273  dvnprodlem2  44274  sge0xp  44756  hoicvr  44875  hoicvrrex  44883  hoidmv1le  44921  hoi2toco  44934  ovnlecvr2  44937  ovolval5lem2  44980  fsetsnf1  45372  setsidel  45654  prproropf1olem3  45783  prproropf1olem4  45784  prproropreud  45787  ushrisomgr  46119  opeliun2xp  46494  lmod1lem2  46655  lmod1lem3  46656  lmod1zr  46660  zlmodzxznm  46664  zlmodzxzldeplem  46665  rrx2xpref1o  46890  line2x  46926  inlinecirc02plem  46958  thincciso  47155  mndtchom  47196
  Copyright terms: Public domain W3C validator