Theorem opex 5397

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 4811	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5369	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5245	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4520	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2833	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 396   ∈ wcel 2105  Vcvv 3440  ∅c0 4266  ifcif 4470  {csn 4570  {cpr 4572  ⟨cop 4576

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577

This theorem is referenced by:  otex  5398  brv  5405  otth2  5416  otthg  5418  sbcop1  5420  oteqex2  5431  oteqex  5432  snopeqop  5438  propeqop  5439  propssopi  5440  euop2  5444  brsnop  5454  brtp  5455  opabidw  5456  opabid  5457  elopab  5459  rexopabb  5460  opabn0  5485  opeliunxp  5672  elvvv  5680  opbrop  5702  relsnopg  5732  xpiindi  5764  raliunxp  5768  idrefALT  6038  intirr  6045  xpnz  6084  dmsnn0  6132  dmsnopg  6138  cnvcnvsn  6144  op2ndb  6152  opswap  6154  cnviin  6211  reuop  6218  dfpo2  6221  funopg  6504  dffv2  6902  fsn  7046  f1o2sn  7053  idref  7057  funsndifnop  7062  fmptsng  7079  fmptsnd  7080  fvsng  7091  resfunexg  7130  fveqf1o  7214  fliftel  7219  fliftel1  7220  oprabidw  7347  oprabid  7348  dfoprab2  7374  oprabv  7376  rnoprab  7419  eloprabga  7423  eloprabgaOLD  7424  ot1stg  7891  ot2ndg  7892  ot3rdg  7893  fo1st  7897  fo2nd  7898  br1steqg  7899  br2ndeqg  7900  opiota  7945  eloprabi  7949  mposn  7989  fpar  8002  fsplitfpar  8004  opco1  8009  opco2  8010  frxp  8012  xporderlem  8013  fnwelem  8017  fvproj  8020  fimaproj  8021  mpoxopoveq  8083  brtpos  8099  dmtpos  8102  rntpos  8103  tpostpos  8110  wfrlem14OLD  8201  tfrlem11  8267  seqomlem1  8329  seqomlem3  8331  seqomlem4  8332  omeu  8465  iiner  8627  xpsnen  8898  xpcomco  8905  xpassen  8909  xpmapenlem  8987  dif1en  9003  dif1enOLD  9005  unxpdomlem1  9093  inlresf  9749  inrresf  9751  djur  9754  djuss  9755  djuun  9761  1stinl  9762  2ndinl  9763  1stinr  9764  2ndinr  9765  fseqenlem2  9860  dju1dif  10007  fpwwe  10481  addpipq2  10771  addpqnq  10773  mulpipq2  10774  mulpqnq  10776  ordpipq  10777  prlem934  10868  addcnsr  10970  mulcnsr  10971  ltresr  10975  addcnsrec  10978  mulcnsrec  10979  axcnre  10999  om2uzrdg  13755  uzrdg0i  13758  uzrdgsuci  13759  hashfun  14230  wrdexb  14306  s1len  14388  s1nz  14389  s111  14397  wrdlen2i  14731  brintclab  14788  fsumcnv  15561  fprodcnv  15769  ruclem1  16016  ruclem4  16019  eucalgval2  16360  crth  16553  phimullem  16554  setsval  16942  setsdm  16945  setsfun  16946  setsfun0  16947  setsexstruct2  16950  setsres  16953  setscom  16955  strfv  16979  setsid  16983  imasaddfnlem  17313  imasaddvallem  17314  imasvscafn  17322  idfuval  17665  cofuval  17671  resfval  17681  resfval2  17682  elhoma  17821  embedsetcestrclem  17948  xpcco  17974  xpcid  17980  1stfval  17982  2ndfval  17985  prfval  17990  prf1  17991  prf2  17993  evlfval  18009  curfval  18015  curf1  18017  curfcl  18024  hofval  18044  intopsn  18412  mgm1  18416  sgrp1  18458  mnd1  18500  mnd1id  18501  grpss  18670  grp1  18755  symg2bas  19073  efgmval  19390  efgi  19397  efgi2  19403  frgpnabllem1  19546  frgpnabllem2  19547  ring1  19913  opsrtoslem2  21343  mat1dimelbas  21700  mat1dimbas  21701  mat1dimscm  21704  mat1dimmul  21705  mat1f1o  21707  mat1rhmelval  21709  mvmulfval  21771  m2detleib  21860  txcnp  22851  upxp  22854  uptx  22856  txdis1cn  22866  hauseqlcld  22877  txlm  22879  xkoinjcn  22918  txflf  23237  qustgplem  23352  ucnima  23513  ucnprima  23514  fmucndlem  23523  imasdsf1olem  23606  cnheiborlem  24197  ovollb2lem  24732  ovolctb  24734  ovolshftlem1  24753  ovolscalem1  24757  ovolicc1  24760  ioombl1lem3  24804  ioombl1lem4  24805  ioorval  24818  dyadval  24836  mbfimaopnlem  24899  limccnp2  25136  brbtwn  27400  brcgr  27401  eengbas  27482  ebtwntg  27483  ecgrtg  27484  elntg  27485  structvtxval  27524  structgrssvtx  27527  structgrssiedg  27528  gropd  27534  isuhgrop  27573  uhgrunop  27578  upgrop  27597  upgr0eop  27617  upgrunop  27622  umgrunop  27624  isuspgrop  27664  isusgrop  27665  ausgrusgrb  27668  usgr0eop  27746  usgrexmpl  27763  griedg0ssusgr  27765  uhgrspanop  27796  uhgrspan1  27803  upgrres  27806  umgrres  27807  usgrres  27808  upgrres1  27813  umgrres1  27814  usgrres1  27815  usgrexi  27941  cusgrexi  27943  cffldtocusgr  27947  cusgrres  27948  vtxdgop  27970  umgr2v2e  28025  wlkp1lem2  28174  wlkswwlksf1o  28376  wwlksnext  28390  eupth2eucrct  28713  eupthvdres  28731  konigsbergumgr  28747  numclwwlk1lem2fv  28852  numclwlk1lem1  28865  ex-br  28927  ex-fpar  28958  cnnvg  29172  cnnvs  29174  cnnvnm  29175  h2hva  29468  h2hsm  29469  h2hnm  29470  hhssva  29751  hhsssm  29752  hhssnm  29753  hhshsslem1  29761  br8d  31081  xppreima2  31119  aciunf1lem  31130  ofpreima  31133  cnvoprabOLD  31186  linds2eq  31710  smatrcl  31882  smatlem  31883  txomap  31920  qtophaus  31922  hgt750lemb  32772  bnj97  32981  bnj553  33013  bnj966  33059  bnj1442  33164  erdszelem9  33296  erdszelem10  33297  txpconn  33329  txsconnlem  33337  goel  33444  goeleq12bg  33446  gonafv  33447  gonanegoal  33449  sat1el2xp  33476  fmlaomn0  33487  gonan0  33489  goaln0  33490  gonarlem  33491  gonar  33492  goalrlem  33493  goalr  33494  fmla0disjsuc  33495  fmlasucdisj  33496  satffunlem  33498  satffunlem1lem1  33499  satffunlem2lem1  33501  satfv0fvfmla0  33510  sategoelfvb  33516  prv1n  33528  msubval  33622  mvhval  33631  msubvrs  33657  brtpid1  33798  brtpid2  33799  brtpid3  33800  ot21std  33811  ot22ndd  33812  otthne  33813  ralxp3f  33816  sbcoteq1a  33818  br8  33853  br6  33854  br4  33855  dfdm5  33874  dfrn5  33875  elima4  33877  fv1stcnv  33878  fv2ndcnv  33879  xpord2lem  33915  xpord2pred  33918  xpord2ind  33920  xpord3lem  33921  frxp3  33923  xpord3pred  33924  naddcllem  33954  addsval  34196  brtxp  34252  brpprod  34257  brpprod3b  34259  brsset  34261  brtxpsd  34266  dffun10  34286  elfuns  34287  brcart  34304  brimg  34309  brapply  34310  brcup  34311  brcap  34312  brsuccf  34313  brrestrict  34321  dfrecs2  34322  dfrdg4  34323  fvtransport  34404  brcolinear2  34430  colineardim1  34433  brsegle  34480  fvline  34516  ellines  34524  filnetlem3  34639  bj-inftyexpitaufo  35450  bj-inftyexpitaudisj  35453  bj-inftyexpiinv  35456  bj-inftyexpidisj  35458  bj-elccinfty  35462  bj-minftyccb  35473  finxpreclem2  35638  finxp0  35639  finxp1o  35640  finxpreclem3  35641  finxpreclem4  35642  finxpreclem5  35643  finxpreclem6  35644  poimirlem9  35863  poimirlem15  35869  poimirlem17  35871  poimirlem20  35874  poimirlem24  35878  poimirlem28  35882  mblfinlem2  35892  heiborlem6  36051  heiborlem7  36052  heiborlem8  36053  grposnOLD  36117  rngosn3  36159  gidsn  36187  zrdivrng  36188  brxrn  36613  br1cossxrnres  36687  dvhvaddval  39330  dvhvscaval  39339  dibglbN  39406  dihglbcpreN  39540  dihmeetlem4preN  39546  dihmeetlem13N  39559  hdmapfval  40067  elcnvlem  41448  cotrintab  41461  elimaint  41496  snhesn  41633  projf1o  42982  dvnprodlem1  43742  dvnprodlem2  43743  sge0xp  44223  hoicvr  44342  hoicvrrex  44350  hoidmv1le  44388  hoi2toco  44401  ovnlecvr2  44404  ovolval5lem2  44447  fsetsnf1  44816  setsidel  45098  prproropf1olem3  45227  prproropf1olem4  45228  prproropreud  45231  ushrisomgr  45563  opeliun2xp  45938  lmod1lem2  46099  lmod1lem3  46100  lmod1zr  46104  zlmodzxznm  46108  zlmodzxzldeplem  46109  rrx2xpref1o  46334  line2x  46370  inlinecirc02plem  46402  thincciso  46600  mndtchom  46641