Theorem opex 5465

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 4871	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5433	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5308	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4579	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2830	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 397   ∈ wcel 2107  Vcvv 3475  ∅c0 4323  ifcif 4529  {csn 4629  {cpr 4631  ⟨cop 4635

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 5300  ax-nul 5307  ax-pr 5428

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 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636

This theorem is referenced by:  otex  5466  brv  5473  otth2  5484  otthg  5486  sbcop1  5489  oteqex2  5500  oteqex  5501  snopeqop  5507  propeqop  5508  propssopi  5509  euop2  5513  brsnop  5523  brtp  5524  opabidw  5525  opabid  5526  elopab  5528  rexopabb  5529  opabn0  5554  opeliunxp  5744  elvvv  5752  opbrop  5774  relsnopg  5804  xpiindi  5836  raliunxp  5840  idrefALT  6113  intirr  6120  xpnz  6159  dmsnn0  6207  dmsnopg  6213  cnvcnvsn  6219  op2ndb  6227  opswap  6229  cnviin  6286  reuop  6293  dfpo2  6296  funopg  6583  dffv2  6987  fsn  7133  f1o2sn  7140  idref  7144  funsndifnop  7149  fmptsng  7166  fmptsnd  7167  fvsng  7178  resfunexg  7217  fveqf1o  7301  fliftel  7306  fliftel1  7307  oprabidw  7440  oprabid  7441  dfoprab2  7467  oprabv  7469  rnoprab  7512  eloprabga  7516  eloprabgaOLD  7517  ot1stg  7989  ot2ndg  7990  ot3rdg  7991  fo1st  7995  fo2nd  7996  br1steqg  7997  br2ndeqg  7998  opiota  8045  eloprabi  8049  mposn  8089  fpar  8102  fsplitfpar  8104  opco1  8109  opco2  8110  frxp  8112  xporderlem  8113  fnwelem  8117  fvproj  8120  fimaproj  8121  xpord2lem  8128  xpord2pred  8131  xpord2indlem  8133  frxp3  8137  mpoxopoveq  8204  brtpos  8220  dmtpos  8223  rntpos  8224  tpostpos  8231  wfrlem14OLD  8322  tfrlem11  8388  seqomlem1  8450  seqomlem3  8452  seqomlem4  8453  omeu  8585  naddcllem  8675  iiner  8783  xpsnen  9055  xpcomco  9062  xpassen  9066  xpmapenlem  9144  dif1en  9160  dif1enOLD  9162  unxpdomlem1  9250  inlresf  9909  inrresf  9911  djur  9914  djuss  9915  djuun  9921  1stinl  9922  2ndinl  9923  1stinr  9924  2ndinr  9925  fseqenlem2  10020  dju1dif  10167  fpwwe  10641  addpipq2  10931  addpqnq  10933  mulpipq2  10934  mulpqnq  10936  ordpipq  10937  prlem934  11028  addcnsr  11130  mulcnsr  11131  ltresr  11135  addcnsrec  11138  mulcnsrec  11139  axcnre  11159  om2uzrdg  13921  uzrdg0i  13924  uzrdgsuci  13925  hashfun  14397  wrdexb  14475  s1len  14556  s1nz  14557  s111  14565  wrdlen2i  14893  brintclab  14948  fsumcnv  15719  fprodcnv  15927  ruclem1  16174  ruclem4  16177  eucalgval2  16518  crth  16711  phimullem  16712  setsval  17100  setsdm  17103  setsfun  17104  setsfun0  17105  setsexstruct2  17108  setsres  17111  setscom  17113  strfv  17137  setsid  17141  imasaddfnlem  17474  imasaddvallem  17475  imasvscafn  17483  idfuval  17826  cofuval  17832  resfval  17842  resfval2  17843  elhoma  17982  embedsetcestrclem  18109  xpcco  18135  xpcid  18141  1stfval  18143  2ndfval  18146  prfval  18151  prf1  18152  prf2  18154  evlfval  18170  curfval  18176  curf1  18178  curfcl  18185  hofval  18205  intopsn  18573  mgm1  18577  sgrp1  18620  mnd1  18667  mnd1id  18668  grpss  18840  grp1  18930  symg2bas  19260  efgmval  19580  efgi  19587  efgi2  19593  frgpnabllem1  19741  frgpnabllem2  19742  ring1  20122  opsrtoslem2  21617  mat1dimelbas  21973  mat1dimbas  21974  mat1dimscm  21977  mat1dimmul  21978  mat1f1o  21980  mat1rhmelval  21982  mvmulfval  22044  m2detleib  22133  txcnp  23124  upxp  23127  uptx  23129  txdis1cn  23139  hauseqlcld  23150  txlm  23152  xkoinjcn  23191  txflf  23510  qustgplem  23625  ucnima  23786  ucnprima  23787  fmucndlem  23796  imasdsf1olem  23879  cnheiborlem  24470  ovollb2lem  25005  ovolctb  25007  ovolshftlem1  25026  ovolscalem1  25030  ovolicc1  25033  ioombl1lem3  25077  ioombl1lem4  25078  ioorval  25091  dyadval  25109  mbfimaopnlem  25172  limccnp2  25409  addsval  27446  mulsval  27565  precsexlem1  27653  precsexlem2  27654  precsexlem3  27655  brbtwn  28157  brcgr  28158  eengbas  28239  ebtwntg  28240  ecgrtg  28241  elntg  28242  structvtxval  28281  structgrssvtx  28284  structgrssiedg  28285  gropd  28291  isuhgrop  28330  uhgrunop  28335  upgrop  28354  upgr0eop  28374  upgrunop  28379  umgrunop  28381  isuspgrop  28421  isusgrop  28422  ausgrusgrb  28425  usgr0eop  28503  usgrexmpl  28520  griedg0ssusgr  28522  uhgrspanop  28553  uhgrspan1  28560  upgrres  28563  umgrres  28564  usgrres  28565  upgrres1  28570  umgrres1  28571  usgrres1  28572  usgrexi  28698  cusgrexi  28700  cffldtocusgr  28704  cusgrres  28705  vtxdgop  28727  umgr2v2e  28782  wlkp1lem2  28931  wlkswwlksf1o  29133  wwlksnext  29147  eupth2eucrct  29470  eupthvdres  29488  konigsbergumgr  29504  numclwwlk1lem2fv  29609  numclwlk1lem1  29622  ex-br  29684  ex-fpar  29715  cnnvg  29931  cnnvs  29933  cnnvnm  29934  h2hva  30227  h2hsm  30228  h2hnm  30229  hhssva  30510  hhsssm  30511  hhssnm  30512  hhshsslem1  30520  br8d  31839  xppreima2  31876  aciunf1lem  31887  ofpreima  31890  cnvoprabOLD  31945  linds2eq  32497  smatrcl  32776  smatlem  32777  txomap  32814  qtophaus  32816  hgt750lemb  33668  bnj97  33877  bnj553  33909  bnj966  33955  bnj1442  34060  erdszelem9  34190  erdszelem10  34191  txpconn  34223  txsconnlem  34231  goel  34338  goeleq12bg  34340  gonafv  34341  gonanegoal  34343  sat1el2xp  34370  fmlaomn0  34381  gonan0  34383  goaln0  34384  gonarlem  34385  gonar  34386  goalrlem  34387  goalr  34388  fmla0disjsuc  34389  fmlasucdisj  34390  satffunlem  34392  satffunlem1lem1  34393  satffunlem2lem1  34395  satfv0fvfmla0  34404  sategoelfvb  34410  prv1n  34422  msubval  34516  mvhval  34525  msubvrs  34551  brtpid1  34690  brtpid2  34691  brtpid3  34692  br8  34726  br6  34727  br4  34728  dfdm5  34744  dfrn5  34745  elima4  34747  fv1stcnv  34748  fv2ndcnv  34749  brtxp  34852  brpprod  34857  brpprod3b  34859  brsset  34861  brtxpsd  34866  dffun10  34886  elfuns  34887  brcart  34904  brimg  34909  brapply  34910  brcup  34911  brcap  34912  brsuccf  34913  brrestrict  34921  dfrecs2  34922  dfrdg4  34923  fvtransport  35004  brcolinear2  35030  colineardim1  35033  brsegle  35080  fvline  35116  ellines  35124  filnetlem3  35265  bj-inftyexpitaufo  36083  bj-inftyexpitaudisj  36086  bj-inftyexpiinv  36089  bj-inftyexpidisj  36091  bj-elccinfty  36095  bj-minftyccb  36106  finxpreclem2  36271  finxp0  36272  finxp1o  36273  finxpreclem3  36274  finxpreclem4  36275  finxpreclem5  36276  finxpreclem6  36277  poimirlem9  36497  poimirlem15  36503  poimirlem17  36505  poimirlem20  36508  poimirlem24  36512  poimirlem28  36516  mblfinlem2  36526  heiborlem6  36684  heiborlem7  36685  heiborlem8  36686  grposnOLD  36750  rngosn3  36792  gidsn  36820  zrdivrng  36821  brxrn  37244  br1cossxrnres  37318  dvhvaddval  39961  dvhvscaval  39970  dibglbN  40037  dihglbcpreN  40171  dihmeetlem4preN  40177  dihmeetlem13N  40190  hdmapfval  40698  elcnvlem  42352  cotrintab  42365  elimaint  42400  snhesn  42537  projf1o  43896  dvnprodlem1  44662  dvnprodlem2  44663  sge0xp  45145  hoicvr  45264  hoicvrrex  45272  hoidmv1le  45310  hoi2toco  45323  ovnlecvr2  45326  ovolval5lem2  45369  fsetsnf1  45762  setsidel  46044  prproropf1olem3  46173  prproropf1olem4  46174  prproropreud  46177  ushrisomgr  46509  rngqiprngimfv  46783  rngqiprngimf1  46785  opeliun2xp  47008  lmod1lem2  47169  lmod1lem3  47170  lmod1zr  47174  zlmodzxznm  47178  zlmodzxzldeplem  47179  rrx2xpref1o  47404  line2x  47440  inlinecirc02plem  47472  thincciso  47669  mndtchom  47710