Theorem opex 5427

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

Step	Hyp	Ref	Expression
1		dfopif 4837	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5395	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5265	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4542	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2825	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Vcvv 3450  ∅c0 4299  ifcif 4491  {csn 4592  {cpr 4594  ⟨cop 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599

This theorem is referenced by:  otex  5428  brv  5435  otth2  5446  otthg  5448  sbcop1  5451  oteqex2  5462  oteqex  5463  snopeqop  5469  propeqop  5470  propssopi  5471  euop2  5475  brsnop  5485  brtp  5486  opabidw  5487  opabid  5488  elopab  5490  rexopabb  5491  opabn0  5516  opeliunxp  5708  opeliun2xp  5709  elvvv  5717  opbrop  5739  relsnopg  5769  xpiindi  5802  raliunxp  5806  idrefALT  6087  intirr  6094  xpnz  6135  dmsnn0  6183  dmsnopg  6189  cnvcnvsn  6195  op2ndb  6203  opswap  6205  cnviin  6262  reuop  6269  dfpo2  6272  funopg  6553  dffv2  6959  fsn  7110  f1o2sn  7117  idref  7121  funsndifnop  7126  fmptsng  7145  fmptsnd  7146  fvsng  7157  resfunexg  7192  fveqf1o  7280  fliftel  7287  fliftel1  7288  oprabidw  7421  oprabid  7422  dfoprab2  7450  oprabv  7452  rnoprab  7497  eloprabga  7501  ot1stg  7985  ot2ndg  7986  ot3rdg  7987  fo1st  7991  fo2nd  7992  br1steqg  7993  br2ndeqg  7994  opiota  8041  eloprabi  8045  mposn  8085  fpar  8098  fsplitfpar  8100  opco1  8105  opco2  8106  frxp  8108  xporderlem  8109  fnwelem  8113  fvproj  8116  fimaproj  8117  xpord2lem  8124  xpord2pred  8127  xpord2indlem  8129  frxp3  8133  mpoxopoveq  8201  brtpos  8217  dmtpos  8220  rntpos  8221  tpostpos  8228  tfrlem11  8359  seqomlem1  8421  seqomlem3  8423  seqomlem4  8424  omeu  8552  naddcllem  8643  iiner  8765  xpsnen  9029  xpcomco  9036  xpassen  9040  xpmapenlem  9114  dif1en  9130  dif1enOLD  9132  unxpdomlem1  9204  inlresf  9874  inrresf  9876  djur  9879  djuss  9880  djuun  9886  1stinl  9887  2ndinl  9888  1stinr  9889  2ndinr  9890  fseqenlem2  9985  dju1dif  10133  fpwwe  10606  addpipq2  10896  addpqnq  10898  mulpipq2  10899  mulpqnq  10901  ordpipq  10902  prlem934  10993  addcnsr  11095  mulcnsr  11096  ltresr  11100  addcnsrec  11103  mulcnsrec  11104  axcnre  11124  om2uzrdg  13928  uzrdg0i  13931  uzrdgsuci  13932  hashfun  14409  wrdexb  14497  s1len  14578  s1nz  14579  s111  14587  wrdlen2i  14915  brintclab  14974  fsumcnv  15746  fprodcnv  15956  ruclem1  16206  ruclem4  16209  eucalgval2  16558  crth  16755  phimullem  16756  setsval  17144  setsdm  17147  setsfun  17148  setsfun0  17149  setsexstruct2  17152  setsres  17155  setscom  17157  strfv  17180  setsid  17184  imasaddfnlem  17498  imasaddvallem  17499  imasvscafn  17507  idfuval  17845  cofuval  17851  resfval  17861  resfval2  17862  elhoma  18001  embedsetcestrclem  18125  xpcco  18151  xpcid  18157  1stfval  18159  2ndfval  18162  prfval  18167  prf1  18168  prf2  18170  evlfval  18185  curfval  18191  curf1  18193  curfcl  18200  hofval  18220  intopsn  18588  mgm1  18592  sgrp1  18663  mnd1  18713  mnd1id  18714  grpss  18893  grp1  18986  symg2bas  19330  efgmval  19649  efgi  19656  efgi2  19662  frgpnabllem1  19810  frgpnabllem2  19811  ring1  20226  rngqiprngimfv  21215  rngqiprngimf1  21217  opsrtoslem2  21970  mat1dimelbas  22365  mat1dimbas  22366  mat1dimscm  22369  mat1dimmul  22370  mat1f1o  22372  mat1rhmelval  22374  mvmulfval  22436  m2detleib  22525  txcnp  23514  upxp  23517  uptx  23519  txdis1cn  23529  hauseqlcld  23540  txlm  23542  xkoinjcn  23581  txflf  23900  qustgplem  24015  ucnima  24175  ucnprima  24176  fmucndlem  24185  imasdsf1olem  24268  cnheiborlem  24860  ovollb2lem  25396  ovolctb  25398  ovolshftlem1  25417  ovolscalem1  25421  ovolicc1  25424  ioombl1lem3  25468  ioombl1lem4  25469  ioorval  25482  dyadval  25500  mbfimaopnlem  25563  limccnp2  25800  addsval  27876  mulsval  28019  precsexlem1  28116  precsexlem2  28117  precsexlem3  28118  om2noseqrdg  28205  noseqrdg0  28208  noseqrdgsuc  28209  brbtwn  28833  brcgr  28834  eengbas  28915  ebtwntg  28916  ecgrtg  28917  elntg  28918  structvtxval  28955  structgrssvtx  28958  structgrssiedg  28959  gropd  28965  isuhgrop  29004  uhgrunop  29009  upgrop  29028  upgr0eop  29048  upgrunop  29053  umgrunop  29055  isuspgrop  29095  isusgrop  29096  ausgrusgrb  29099  usgr0eop  29180  griedg0ssusgr  29199  uhgrspanop  29230  uhgrspan1  29237  upgrres  29240  umgrres  29241  usgrres  29242  upgrres1  29247  umgrres1  29248  usgrres1  29249  usgrexi  29375  cusgrexi  29377  cffldtocusgr  29381  cffldtocusgrOLD  29382  cusgrres  29383  vtxdgop  29405  umgr2v2e  29460  wlkp1lem2  29609  wlkswwlksf1o  29816  wwlksnext  29830  eupth2eucrct  30153  eupthvdres  30171  konigsbergumgr  30187  numclwwlk1lem2fv  30292  numclwlk1lem1  30305  ex-br  30367  ex-fpar  30398  cnnvg  30614  cnnvs  30616  cnnvnm  30617  h2hva  30910  h2hsm  30911  h2hnm  30912  hhssva  31193  hhsssm  31194  hhssnm  31195  hhshsslem1  31203  br8d  32545  xppreima2  32582  aciunf1lem  32593  ofpreima  32596  rlocaddval  33226  rlocmulval  33227  linds2eq  33359  smatrcl  33793  smatlem  33794  txomap  33831  qtophaus  33833  hgt750lemb  34654  bnj97  34863  bnj553  34895  bnj966  34941  bnj1442  35046  erdszelem9  35193  erdszelem10  35194  txpconn  35226  txsconnlem  35234  goel  35341  goeleq12bg  35343  gonafv  35344  gonanegoal  35346  sat1el2xp  35373  fmlaomn0  35384  gonan0  35386  goaln0  35387  gonarlem  35388  gonar  35389  goalrlem  35390  goalr  35391  fmla0disjsuc  35392  fmlasucdisj  35393  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  satfv0fvfmla0  35407  sategoelfvb  35413  prv1n  35425  msubval  35519  mvhval  35528  msubvrs  35554  brtpid1  35715  brtpid2  35716  brtpid3  35717  br8  35750  br6  35751  br4  35752  dfdm5  35767  dfrn5  35768  elima4  35770  fv1stcnv  35771  fv2ndcnv  35772  brtxp  35875  brpprod  35880  brpprod3b  35882  brsset  35884  brtxpsd  35889  dffun10  35909  elfuns  35910  brcart  35927  brimg  35932  brapply  35933  brcup  35934  brcap  35935  brsuccf  35936  brrestrict  35944  dfrecs2  35945  dfrdg4  35946  fvtransport  36027  brcolinear2  36053  colineardim1  36056  brsegle  36103  fvline  36139  ellines  36147  filnetlem3  36375  bj-inftyexpitaufo  37197  bj-inftyexpitaudisj  37200  bj-inftyexpiinv  37203  bj-inftyexpidisj  37205  bj-elccinfty  37209  bj-minftyccb  37220  finxpreclem2  37385  finxp0  37386  finxp1o  37387  finxpreclem3  37388  finxpreclem4  37389  finxpreclem5  37390  finxpreclem6  37391  poimirlem9  37630  poimirlem15  37636  poimirlem17  37638  poimirlem20  37641  poimirlem24  37645  poimirlem28  37649  mblfinlem2  37659  heiborlem6  37817  heiborlem7  37818  heiborlem8  37819  grposnOLD  37883  rngosn3  37925  gidsn  37953  zrdivrng  37954  brxrn  38363  br1cossxrnres  38446  dvhvaddval  41091  dvhvscaval  41100  dibglbN  41167  dihglbcpreN  41301  dihmeetlem4preN  41307  dihmeetlem13N  41320  hdmapfval  41828  elcnvlem  43597  cotrintab  43610  elimaint  43645  snhesn  43782  nregmodellem  45013  projf1o  45198  dvnprodlem1  45951  dvnprodlem2  45952  sge0xp  46434  hoicvr  46553  hoicvrrex  46561  hoidmv1le  46599  hoi2toco  46612  ovnlecvr2  46615  ovolval5lem2  46658  fsetsnf1  47057  setsidel  47381  prproropf1olem3  47510  prproropf1olem4  47511  prproropreud  47514  isisubgr  47866  ushggricedg  47931  gpgusgralem  48051  gpgvtxedg0  48058  gpgvtxedg1  48059  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg3nbgrvtx0  48071  gpg3nbgrvtx0ALT  48072  gpg3nbgrvtx1  48073  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  gpg3kgrtriex  48084  gpgprismgr4cycllem2  48090  gpgprismgr4cycllem6  48094  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem10  48098  lmod1lem2  48481  lmod1lem3  48482  lmod1zr  48486  zlmodzxznm  48490  zlmodzxzldeplem  48491  rrx2xpref1o  48711  line2x  48747  inlinecirc02plem  48779  iinxp  48823  ovsng  48850  eloprab1st2nd  48860  tposid  48877  tposidres  48878  initc  49084  rescofuf  49086  idfurcl  49091  imaf1hom  49101  oppffn  49117  oppfvalg  49119  swapfval  49255  swapf1a  49262  swapf2a  49264  swapf1  49265  swapf2  49267  fucofvalg  49311  fucofval  49312  fucofvalne  49318  fuco21  49329  fucof21  49340  prcofvalg  49369  prcofvala  49370  prcofval  49371  thincciso  49446  setc1ocofval  49487  functermceu  49503  termcfuncval  49525  fucterm  49535  0fucterm  49536  relran  49617  ranval3  49624  ranrcl4lem  49631  ranup  49635  initocmd  49662