Theorem opex 5411

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Vcvv 3438  ∅c0 4286  ifcif 4478  {csn 4579  {cpr 4581  ⟨cop 4585

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 2701  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 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  otex  5412  brv  5419  otth2  5430  otthg  5432  sbcop1  5435  oteqex2  5446  oteqex  5447  snopeqop  5453  propeqop  5454  propssopi  5455  euop2  5459  brsnop  5469  brtp  5470  opabidw  5471  opabid  5472  elopab  5474  rexopabb  5475  opabn0  5500  opeliunxp  5690  opeliun2xp  5691  elvvv  5699  opbrop  5721  relsnopg  5750  xpiindi  5782  raliunxp  5786  idrefALT  6066  intirr  6071  xpnz  6112  dmsnn0  6160  dmsnopg  6166  cnvcnvsn  6172  op2ndb  6180  opswap  6182  cnviin  6238  reuop  6245  dfpo2  6248  funopg  6520  dffv2  6922  fsn  7073  f1o2sn  7080  idref  7084  funsndifnop  7089  fmptsng  7108  fmptsnd  7109  fvsng  7120  resfunexg  7155  fveqf1o  7243  fliftel  7250  fliftel1  7251  oprabidw  7384  oprabid  7385  dfoprab2  7411  oprabv  7413  rnoprab  7458  eloprabga  7462  ot1stg  7945  ot2ndg  7946  ot3rdg  7947  fo1st  7951  fo2nd  7952  br1steqg  7953  br2ndeqg  7954  opiota  8001  eloprabi  8005  mposn  8043  fpar  8056  fsplitfpar  8058  opco1  8063  opco2  8064  frxp  8066  xporderlem  8067  fnwelem  8071  fvproj  8074  fimaproj  8075  xpord2lem  8082  xpord2pred  8085  xpord2indlem  8087  frxp3  8091  mpoxopoveq  8159  brtpos  8175  dmtpos  8178  rntpos  8179  tpostpos  8186  tfrlem11  8317  seqomlem1  8379  seqomlem3  8381  seqomlem4  8382  omeu  8510  naddcllem  8601  iiner  8723  xpsnen  8985  xpcomco  8991  xpassen  8995  xpmapenlem  9068  dif1en  9084  dif1enOLD  9086  unxpdomlem1  9155  inlresf  9829  inrresf  9831  djur  9834  djuss  9835  djuun  9841  1stinl  9842  2ndinl  9843  1stinr  9844  2ndinr  9845  fseqenlem2  9938  dju1dif  10086  fpwwe  10559  addpipq2  10849  addpqnq  10851  mulpipq2  10852  mulpqnq  10854  ordpipq  10855  prlem934  10946  addcnsr  11048  mulcnsr  11049  ltresr  11053  addcnsrec  11056  mulcnsrec  11057  axcnre  11077  om2uzrdg  13881  uzrdg0i  13884  uzrdgsuci  13885  hashfun  14362  wrdexb  14450  s1len  14531  s1nz  14532  s111  14540  wrdlen2i  14867  brintclab  14926  fsumcnv  15698  fprodcnv  15908  ruclem1  16158  ruclem4  16161  eucalgval2  16510  crth  16707  phimullem  16708  setsval  17096  setsdm  17099  setsfun  17100  setsfun0  17101  setsexstruct2  17104  setsres  17107  setscom  17109  strfv  17132  setsid  17136  imasaddfnlem  17450  imasaddvallem  17451  imasvscafn  17459  idfuval  17801  cofuval  17807  resfval  17817  resfval2  17818  elhoma  17957  embedsetcestrclem  18081  xpcco  18107  xpcid  18113  1stfval  18115  2ndfval  18118  prfval  18123  prf1  18124  prf2  18126  evlfval  18141  curfval  18147  curf1  18149  curfcl  18156  hofval  18176  intopsn  18546  mgm1  18550  sgrp1  18621  mnd1  18671  mnd1id  18672  grpss  18851  grp1  18944  symg2bas  19290  efgmval  19609  efgi  19616  efgi2  19622  frgpnabllem1  19770  frgpnabllem2  19771  ring1  20213  rngqiprngimfv  21223  rngqiprngimf1  21225  opsrtoslem2  21979  mat1dimelbas  22374  mat1dimbas  22375  mat1dimscm  22378  mat1dimmul  22379  mat1f1o  22381  mat1rhmelval  22383  mvmulfval  22445  m2detleib  22534  txcnp  23523  upxp  23526  uptx  23528  txdis1cn  23538  hauseqlcld  23549  txlm  23551  xkoinjcn  23590  txflf  23909  qustgplem  24024  ucnima  24184  ucnprima  24185  fmucndlem  24194  imasdsf1olem  24277  cnheiborlem  24869  ovollb2lem  25405  ovolctb  25407  ovolshftlem1  25426  ovolscalem1  25430  ovolicc1  25433  ioombl1lem3  25477  ioombl1lem4  25478  ioorval  25491  dyadval  25509  mbfimaopnlem  25572  limccnp2  25809  addsval  27892  mulsval  28035  precsexlem1  28132  precsexlem2  28133  precsexlem3  28134  om2noseqrdg  28221  noseqrdg0  28224  noseqrdgsuc  28225  brbtwn  28862  brcgr  28863  eengbas  28944  ebtwntg  28945  ecgrtg  28946  elntg  28947  structvtxval  28984  structgrssvtx  28987  structgrssiedg  28988  gropd  28994  isuhgrop  29033  uhgrunop  29038  upgrop  29057  upgr0eop  29077  upgrunop  29082  umgrunop  29084  isuspgrop  29124  isusgrop  29125  ausgrusgrb  29128  usgr0eop  29209  griedg0ssusgr  29228  uhgrspanop  29259  uhgrspan1  29266  upgrres  29269  umgrres  29270  usgrres  29271  upgrres1  29276  umgrres1  29277  usgrres1  29278  usgrexi  29404  cusgrexi  29406  cffldtocusgr  29410  cffldtocusgrOLD  29411  cusgrres  29412  vtxdgop  29434  umgr2v2e  29489  wlkp1lem2  29636  wlkswwlksf1o  29842  wwlksnext  29856  eupth2eucrct  30179  eupthvdres  30197  konigsbergumgr  30213  numclwwlk1lem2fv  30318  numclwlk1lem1  30331  ex-br  30393  ex-fpar  30424  cnnvg  30640  cnnvs  30642  cnnvnm  30643  h2hva  30936  h2hsm  30937  h2hnm  30938  hhssva  31219  hhsssm  31220  hhssnm  31221  hhshsslem1  31229  br8d  32571  xppreima2  32608  aciunf1lem  32619  ofpreima  32622  rlocaddval  33221  rlocmulval  33222  linds2eq  33331  smatrcl  33765  smatlem  33766  txomap  33803  qtophaus  33805  hgt750lemb  34626  bnj97  34835  bnj553  34867  bnj966  34913  bnj1442  35018  erdszelem9  35174  erdszelem10  35175  txpconn  35207  txsconnlem  35215  goel  35322  goeleq12bg  35324  gonafv  35325  gonanegoal  35327  sat1el2xp  35354  fmlaomn0  35365  gonan0  35367  goaln0  35368  gonarlem  35369  gonar  35370  goalrlem  35371  goalr  35372  fmla0disjsuc  35373  fmlasucdisj  35374  satffunlem  35376  satffunlem1lem1  35377  satffunlem2lem1  35379  satfv0fvfmla0  35388  sategoelfvb  35394  prv1n  35406  msubval  35500  mvhval  35509  msubvrs  35535  brtpid1  35696  brtpid2  35697  brtpid3  35698  br8  35731  br6  35732  br4  35733  dfdm5  35748  dfrn5  35749  elima4  35751  fv1stcnv  35752  fv2ndcnv  35753  brtxp  35856  brpprod  35861  brpprod3b  35863  brsset  35865  brtxpsd  35870  dffun10  35890  elfuns  35891  brcart  35908  brimg  35913  brapply  35914  brcup  35915  brcap  35916  brsuccf  35917  brrestrict  35925  dfrecs2  35926  dfrdg4  35927  fvtransport  36008  brcolinear2  36034  colineardim1  36037  brsegle  36084  fvline  36120  ellines  36128  filnetlem3  36356  bj-inftyexpitaufo  37178  bj-inftyexpitaudisj  37181  bj-inftyexpiinv  37184  bj-inftyexpidisj  37186  bj-elccinfty  37190  bj-minftyccb  37201  finxpreclem2  37366  finxp0  37367  finxp1o  37368  finxpreclem3  37369  finxpreclem4  37370  finxpreclem5  37371  finxpreclem6  37372  poimirlem9  37611  poimirlem15  37617  poimirlem17  37619  poimirlem20  37622  poimirlem24  37626  poimirlem28  37630  mblfinlem2  37640  heiborlem6  37798  heiborlem7  37799  heiborlem8  37800  grposnOLD  37864  rngosn3  37906  gidsn  37934  zrdivrng  37935  brxrn  38344  br1cossxrnres  38427  dvhvaddval  41072  dvhvscaval  41081  dibglbN  41148  dihglbcpreN  41282  dihmeetlem4preN  41288  dihmeetlem13N  41301  hdmapfval  41809  elcnvlem  43577  cotrintab  43590  elimaint  43625  snhesn  43762  nregmodellem  44993  projf1o  45178  dvnprodlem1  45931  dvnprodlem2  45932  sge0xp  46414  hoicvr  46533  hoicvrrex  46541  hoidmv1le  46579  hoi2toco  46592  ovnlecvr2  46595  ovolval5lem2  46638  fsetsnf1  47040  setsidel  47364  prproropf1olem3  47493  prproropf1olem4  47494  prproropreud  47497  isisubgr  47850  ushggricedg  47915  gpgusgralem  48044  gpgvtxedg0  48051  gpgvtxedg1  48052  gpg5nbgrvtx03starlem1  48056  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem2  48060  gpg5nbgrvtx13starlem3  48061  gpg3nbgrvtx0  48064  gpg3nbgrvtx0ALT  48065  gpg3nbgrvtx1  48066  gpg5nbgrvtx03star  48068  gpg5nbgr3star  48069  gpg3kgrtriex  48077  gpgprismgr4cycllem2  48084  gpgprismgr4cycllem6  48088  gpgprismgr4cycllem7  48089  gpgprismgr4cycllem10  48092  gpg5edgnedg  48118  lmod1lem2  48477  lmod1lem3  48478  lmod1zr  48482  zlmodzxznm  48486  zlmodzxzldeplem  48487  rrx2xpref1o  48707  line2x  48743  inlinecirc02plem  48775  iinxp  48819  ovsng  48846  eloprab1st2nd  48856  tposid  48873  tposidres  48874  initc  49080  rescofuf  49082  idfurcl  49087  imaf1hom  49097  oppffn  49113  oppfvalg  49115  swapfval  49251  swapf1a  49258  swapf2a  49260  swapf1  49261  swapf2  49263  fucofvalg  49307  fucofval  49308  fucofvalne  49314  fuco21  49325  fucof21  49336  prcofvalg  49365  prcofvala  49366  prcofval  49367  thincciso  49442  setc1ocofval  49483  functermceu  49499  termcfuncval  49521  fucterm  49531  0fucterm  49532  relran  49613  ranval3  49620  ranrcl4lem  49627  ranup  49631  initocmd  49658