Theorem opex 5409

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 4823	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5379	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5249	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4527	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2829	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2113  Vcvv 3437  ∅c0 4282  ifcif 4476  {csn 4577  {cpr 4579  ⟨cop 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584

This theorem is referenced by:  otex  5410  brv  5417  otth2  5428  otthg  5430  sbcop1  5433  oteqex2  5444  oteqex  5445  snopeqop  5451  propeqop  5452  propssopi  5453  euop2  5457  brsnop  5467  brtp  5468  opabidw  5469  opabid  5470  elopab  5472  rexopabb  5473  opabn0  5498  opeliunxp  5688  opeliun2xp  5689  elvvv  5697  opbrop  5719  relsnopg  5749  xpiindi  5781  raliunxp  5785  idrefALT  6066  intirr  6071  xpnz  6113  dmsnn0  6161  dmsnopg  6167  cnvcnvsn  6173  op2ndb  6181  opswap  6183  cnviin  6240  reuop  6247  dfpo2  6250  funopg  6522  dffv2  6925  fsn  7076  f1o2sn  7083  idref  7087  funsndifnop  7092  fmptsng  7110  fmptsnd  7111  fvsng  7122  resfunexg  7157  fveqf1o  7244  fliftel  7251  fliftel1  7252  oprabidw  7385  oprabid  7386  dfoprab2  7412  oprabv  7414  rnoprab  7459  eloprabga  7463  ot1stg  7943  ot2ndg  7944  ot3rdg  7945  fo1st  7949  fo2nd  7950  br1steqg  7951  br2ndeqg  7952  opiota  7999  eloprabi  8003  mposn  8041  fpar  8054  fsplitfpar  8056  opco1  8061  opco2  8062  frxp  8064  xporderlem  8065  fnwelem  8069  fvproj  8072  fimaproj  8073  xpord2lem  8080  xpord2pred  8083  xpord2indlem  8085  frxp3  8089  mpoxopoveq  8157  brtpos  8173  dmtpos  8176  rntpos  8177  tpostpos  8184  tfrlem11  8315  seqomlem1  8377  seqomlem3  8379  seqomlem4  8380  omeu  8508  naddcllem  8599  iiner  8721  xpsnen  8983  xpcomco  8989  xpassen  8993  xpmapenlem  9066  dif1en  9080  unxpdomlem1  9149  inlresf  9816  inrresf  9818  djur  9821  djuss  9822  djuun  9828  1stinl  9829  2ndinl  9830  1stinr  9831  2ndinr  9832  fseqenlem2  9925  dju1dif  10073  fpwwe  10546  addpipq2  10836  addpqnq  10838  mulpipq2  10839  mulpqnq  10841  ordpipq  10842  prlem934  10933  addcnsr  11035  mulcnsr  11036  ltresr  11040  addcnsrec  11043  mulcnsrec  11044  axcnre  11064  om2uzrdg  13867  uzrdg0i  13870  uzrdgsuci  13871  hashfun  14348  wrdexb  14436  s1len  14518  s1nz  14519  s111  14527  wrdlen2i  14853  brintclab  14912  fsumcnv  15684  fprodcnv  15894  ruclem1  16144  ruclem4  16147  eucalgval2  16496  crth  16693  phimullem  16694  setsval  17082  setsdm  17085  setsfun  17086  setsfun0  17087  setsexstruct2  17090  setsres  17093  setscom  17095  strfv  17118  setsid  17122  imasaddfnlem  17436  imasaddvallem  17437  imasvscafn  17445  idfuval  17787  cofuval  17793  resfval  17803  resfval2  17804  elhoma  17943  embedsetcestrclem  18067  xpcco  18093  xpcid  18099  1stfval  18101  2ndfval  18104  prfval  18109  prf1  18110  prf2  18112  evlfval  18127  curfval  18133  curf1  18135  curfcl  18142  hofval  18162  intopsn  18566  mgm1  18570  sgrp1  18641  mnd1  18691  mnd1id  18692  grpss  18871  grp1  18964  symg2bas  19309  efgmval  19628  efgi  19635  efgi2  19641  frgpnabllem1  19789  frgpnabllem2  19790  ring1  20232  rngqiprngimfv  21239  rngqiprngimf1  21241  opsrtoslem2  21994  mat1dimelbas  22389  mat1dimbas  22390  mat1dimscm  22393  mat1dimmul  22394  mat1f1o  22396  mat1rhmelval  22398  mvmulfval  22460  m2detleib  22549  txcnp  23538  upxp  23541  uptx  23543  txdis1cn  23553  hauseqlcld  23564  txlm  23566  xkoinjcn  23605  txflf  23924  qustgplem  24039  ucnima  24198  ucnprima  24199  fmucndlem  24208  imasdsf1olem  24291  cnheiborlem  24883  ovollb2lem  25419  ovolctb  25421  ovolshftlem1  25440  ovolscalem1  25444  ovolicc1  25447  ioombl1lem3  25491  ioombl1lem4  25492  ioorval  25505  dyadval  25523  mbfimaopnlem  25586  limccnp2  25823  addsval  27908  mulsval  28051  precsexlem1  28148  precsexlem2  28149  precsexlem3  28150  om2noseqrdg  28237  noseqrdg0  28240  noseqrdgsuc  28241  brbtwn  28881  brcgr  28882  eengbas  28963  ebtwntg  28964  ecgrtg  28965  elntg  28966  structvtxval  29003  structgrssvtx  29006  structgrssiedg  29007  gropd  29013  isuhgrop  29052  uhgrunop  29057  upgrop  29076  upgr0eop  29096  upgrunop  29101  umgrunop  29103  isuspgrop  29143  isusgrop  29144  ausgrusgrb  29147  usgr0eop  29228  griedg0ssusgr  29247  uhgrspanop  29278  uhgrspan1  29285  upgrres  29288  umgrres  29289  usgrres  29290  upgrres1  29295  umgrres1  29296  usgrres1  29297  usgrexi  29423  cusgrexi  29425  cffldtocusgr  29429  cffldtocusgrOLD  29430  cusgrres  29431  vtxdgop  29453  umgr2v2e  29508  wlkp1lem2  29655  wlkswwlksf1o  29861  wwlksnext  29875  eupth2eucrct  30201  eupthvdres  30219  konigsbergumgr  30235  numclwwlk1lem2fv  30340  numclwlk1lem1  30353  ex-br  30415  ex-fpar  30446  cnnvg  30662  cnnvs  30664  cnnvnm  30665  h2hva  30958  h2hsm  30959  h2hnm  30960  hhssva  31241  hhsssm  31242  hhssnm  31243  hhshsslem1  31251  br8d  32595  xppreima2  32637  aciunf1lem  32648  ofpreima  32651  rlocaddval  33244  rlocmulval  33245  linds2eq  33355  smatrcl  33832  smatlem  33833  txomap  33870  qtophaus  33872  hgt750lemb  34692  bnj97  34901  bnj553  34933  bnj966  34979  bnj1442  35084  erdszelem9  35266  erdszelem10  35267  txpconn  35299  txsconnlem  35307  goel  35414  goeleq12bg  35416  gonafv  35417  gonanegoal  35419  sat1el2xp  35446  fmlaomn0  35457  gonan0  35459  goaln0  35460  gonarlem  35461  gonar  35462  goalrlem  35463  goalr  35464  fmla0disjsuc  35465  fmlasucdisj  35466  satffunlem  35468  satffunlem1lem1  35469  satffunlem2lem1  35471  satfv0fvfmla0  35480  sategoelfvb  35486  prv1n  35498  msubval  35592  mvhval  35601  msubvrs  35627  brtpid1  35788  brtpid2  35789  brtpid3  35790  br8  35823  br6  35824  br4  35825  dfdm5  35840  dfrn5  35841  elima4  35843  fv1stcnv  35844  fv2ndcnv  35845  brtxp  35945  brpprod  35950  brpprod3b  35952  brsset  35954  brtxpsd  35959  dffun10  35979  elfuns  35980  brcart  35997  brimg  36002  brapply  36003  brcup  36004  brcap  36005  lemsuccf  36006  brrestrict  36016  dfrecs2  36017  dfrdg4  36018  fvtransport  36099  brcolinear2  36125  colineardim1  36128  brsegle  36175  fvline  36211  ellines  36219  filnetlem3  36447  bj-inftyexpitaufo  37269  bj-inftyexpitaudisj  37272  bj-inftyexpiinv  37275  bj-inftyexpidisj  37277  bj-elccinfty  37281  bj-minftyccb  37292  finxpreclem2  37457  finxp0  37458  finxp1o  37459  finxpreclem3  37460  finxpreclem4  37461  finxpreclem5  37462  finxpreclem6  37463  poimirlem9  37692  poimirlem15  37698  poimirlem17  37700  poimirlem20  37703  poimirlem24  37707  poimirlem28  37711  mblfinlem2  37721  heiborlem6  37879  heiborlem7  37880  heiborlem8  37881  grposnOLD  37945  rngosn3  37987  gidsn  38015  zrdivrng  38016  brxrn  38430  ecxrn2  38455  br1cossxrnres  38573  dvhvaddval  41212  dvhvscaval  41221  dibglbN  41288  dihglbcpreN  41422  dihmeetlem4preN  41428  dihmeetlem13N  41441  hdmapfval  41949  elcnvlem  43721  cotrintab  43734  elimaint  43769  snhesn  43906  nregmodellem  45136  projf1o  45321  dvnprodlem1  46071  dvnprodlem2  46072  sge0xp  46554  hoicvr  46673  hoicvrrex  46681  hoidmv1le  46719  hoi2toco  46732  ovnlecvr2  46735  ovolval5lem2  46778  fsetsnf1  47179  setsidel  47503  prproropf1olem3  47632  prproropf1olem4  47633  prproropreud  47636  isisubgr  47989  ushggricedg  48054  gpgusgralem  48183  gpgvtxedg0  48190  gpgvtxedg1  48191  gpg5nbgrvtx03starlem1  48195  gpg5nbgrvtx03starlem2  48196  gpg5nbgrvtx03starlem3  48197  gpg5nbgrvtx13starlem1  48198  gpg5nbgrvtx13starlem2  48199  gpg5nbgrvtx13starlem3  48200  gpg3nbgrvtx0  48203  gpg3nbgrvtx0ALT  48204  gpg3nbgrvtx1  48205  gpg5nbgrvtx03star  48207  gpg5nbgr3star  48208  gpg3kgrtriex  48216  gpgprismgr4cycllem2  48223  gpgprismgr4cycllem6  48227  gpgprismgr4cycllem7  48228  gpgprismgr4cycllem10  48231  gpg5edgnedg  48257  lmod1lem2  48616  lmod1lem3  48617  lmod1zr  48621  zlmodzxznm  48625  zlmodzxzldeplem  48626  rrx2xpref1o  48846  line2x  48882  inlinecirc02plem  48914  iinxp  48958  ovsng  48985  eloprab1st2nd  48995  tposid  49012  tposidres  49013  initc  49219  rescofuf  49221  idfurcl  49226  imaf1hom  49236  oppffn  49252  oppfvalg  49254  swapfval  49390  swapf1a  49397  swapf2a  49399  swapf1  49400  swapf2  49402  fucofvalg  49446  fucofval  49447  fucofvalne  49453  fuco21  49464  fucof21  49475  prcofvalg  49504  prcofvala  49505  prcofval  49506  thincciso  49581  setc1ocofval  49622  functermceu  49638  termcfuncval  49660  fucterm  49670  0fucterm  49671  relran  49752  ranval3  49759  ranrcl4lem  49766  ranup  49770  initocmd  49797