Theorem opex 5379

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 4800	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5355	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5231	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4509	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2835	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 396   ∈ wcel 2106  Vcvv 3432  ∅c0 4256  ifcif 4459  {csn 4561  {cpr 4563  ⟨cop 4567

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568

This theorem is referenced by:  otex  5380  brv  5387  otth2  5398  otthg  5400  sbcop1  5402  oteqex2  5413  oteqex  5414  snopeqop  5420  propeqop  5421  propssopi  5422  euop2  5426  brsnop  5436  opabidw  5437  opabid  5438  elopab  5440  rexopabb  5441  opabn0  5466  opeliunxp  5654  elvvv  5662  opbrop  5684  relsnopg  5713  xpiindi  5744  raliunxp  5748  idrefALT  6018  intirr  6023  xpnz  6062  dmsnn0  6110  dmsnopg  6116  cnvcnvsn  6122  op2ndb  6130  opswap  6132  cnviin  6189  reuop  6196  dfpo2  6199  funopg  6468  dffv2  6863  fsn  7007  f1o2sn  7014  idref  7018  funsndifnop  7023  fmptsng  7040  fmptsnd  7041  fvsng  7052  resfunexg  7091  fveqf1o  7175  fliftel  7180  fliftel1  7181  oprabidw  7306  oprabid  7307  dfoprab2  7333  oprabv  7335  rnoprab  7378  eloprabga  7382  eloprabgaOLD  7383  ot1stg  7845  ot2ndg  7846  ot3rdg  7847  fo1st  7851  fo2nd  7852  br1steqg  7853  br2ndeqg  7854  opiota  7899  eloprabi  7903  mposn  7943  fpar  7956  fsplitfpar  7959  opco1  7964  opco2  7965  frxp  7967  xporderlem  7968  fnwelem  7972  fvproj  7975  fimaproj  7976  mpoxopoveq  8035  brtpos  8051  dmtpos  8054  rntpos  8055  tpostpos  8062  wfrlem14OLD  8153  tfrlem11  8219  seqomlem1  8281  seqomlem3  8283  seqomlem4  8284  omeu  8416  iiner  8578  xpsnen  8842  xpcomco  8849  xpassen  8853  xpmapenlem  8931  dif1en  8945  unxpdomlem1  9027  inlresf  9672  inrresf  9674  djur  9677  djuss  9678  djuun  9684  1stinl  9685  2ndinl  9686  1stinr  9687  2ndinr  9688  fseqenlem2  9781  dju1dif  9928  fpwwe  10402  addpipq2  10692  addpqnq  10694  mulpipq2  10695  mulpqnq  10697  ordpipq  10698  prlem934  10789  addcnsr  10891  mulcnsr  10892  ltresr  10896  addcnsrec  10899  mulcnsrec  10900  axcnre  10920  om2uzrdg  13676  uzrdg0i  13679  uzrdgsuci  13680  hashfun  14152  wrdexb  14228  s1len  14311  s1nz  14312  s111  14320  wrdlen2i  14655  brintclab  14712  fsumcnv  15485  fprodcnv  15693  ruclem1  15940  ruclem4  15943  eucalgval2  16286  crth  16479  phimullem  16480  setsval  16868  setsdm  16871  setsfun  16872  setsfun0  16873  setsexstruct2  16876  setsres  16879  setscom  16881  strfv  16905  setsid  16909  imasaddfnlem  17239  imasaddvallem  17240  imasvscafn  17248  idfuval  17591  cofuval  17597  resfval  17607  resfval2  17608  elhoma  17747  embedsetcestrclem  17874  xpcco  17900  xpcid  17906  1stfval  17908  2ndfval  17911  prfval  17916  prf1  17917  prf2  17919  evlfval  17935  curfval  17941  curf1  17943  curfcl  17950  hofval  17970  intopsn  18338  mgm1  18342  sgrp1  18384  mnd1  18426  mnd1id  18427  grpss  18597  grp1  18682  symg2bas  19000  efgmval  19318  efgi  19325  efgi2  19331  frgpnabllem1  19474  frgpnabllem2  19475  ring1  19841  opsrtoslem2  21263  mat1dimelbas  21620  mat1dimbas  21621  mat1dimscm  21624  mat1dimmul  21625  mat1f1o  21627  mat1rhmelval  21629  mvmulfval  21691  m2detleib  21780  txcnp  22771  upxp  22774  uptx  22776  txdis1cn  22786  hauseqlcld  22797  txlm  22799  xkoinjcn  22838  txflf  23157  qustgplem  23272  ucnima  23433  ucnprima  23434  fmucndlem  23443  imasdsf1olem  23526  cnheiborlem  24117  ovollb2lem  24652  ovolctb  24654  ovolshftlem1  24673  ovolscalem1  24677  ovolicc1  24680  ioombl1lem3  24724  ioombl1lem4  24725  ioorval  24738  dyadval  24756  mbfimaopnlem  24819  limccnp2  25056  brbtwn  27267  brcgr  27268  eengbas  27349  ebtwntg  27350  ecgrtg  27351  elntg  27352  structvtxval  27391  structgrssvtx  27394  structgrssiedg  27395  gropd  27401  isuhgrop  27440  uhgrunop  27445  upgrop  27464  upgr0eop  27484  upgrunop  27489  umgrunop  27491  isuspgrop  27531  isusgrop  27532  ausgrusgrb  27535  usgr0eop  27613  usgrexmpl  27630  griedg0ssusgr  27632  uhgrspanop  27663  uhgrspan1  27670  upgrres  27673  umgrres  27674  usgrres  27675  upgrres1  27680  umgrres1  27681  usgrres1  27682  usgrexi  27808  cusgrexi  27810  cffldtocusgr  27814  cusgrres  27815  vtxdgop  27837  umgr2v2e  27892  wlkp1lem2  28042  wlkswwlksf1o  28244  wwlksnext  28258  eupth2eucrct  28581  eupthvdres  28599  konigsbergumgr  28615  numclwwlk1lem2fv  28720  numclwlk1lem1  28733  ex-br  28795  ex-fpar  28826  cnnvg  29040  cnnvs  29042  cnnvnm  29043  h2hva  29336  h2hsm  29337  h2hnm  29338  hhssva  29619  hhsssm  29620  hhssnm  29621  hhshsslem1  29629  br8d  30950  xppreima2  30988  aciunf1lem  30999  ofpreima  31002  cnvoprabOLD  31055  linds2eq  31575  smatrcl  31746  smatlem  31747  txomap  31784  qtophaus  31786  hgt750lemb  32636  bnj97  32846  bnj553  32878  bnj966  32924  bnj1442  33029  erdszelem9  33161  erdszelem10  33162  txpconn  33194  txsconnlem  33202  goel  33309  goeleq12bg  33311  gonafv  33312  gonanegoal  33314  sat1el2xp  33341  fmlaomn0  33352  gonan0  33354  goaln0  33355  gonarlem  33356  gonar  33357  goalrlem  33358  goalr  33359  fmla0disjsuc  33360  fmlasucdisj  33361  satffunlem  33363  satffunlem1lem1  33364  satffunlem2lem1  33366  satfv0fvfmla0  33375  sategoelfvb  33381  prv1n  33393  msubval  33487  mvhval  33496  msubvrs  33522  brtpid1  33665  brtpid2  33666  brtpid3  33667  ot21std  33680  ot22ndd  33681  otthne  33682  ralxp3f  33685  sbcoteq1a  33687  brtp  33717  br8  33723  br6  33724  br4  33725  dfdm5  33747  dfrn5  33748  elima4  33750  fv1stcnv  33751  fv2ndcnv  33752  xpord2lem  33789  xpord2pred  33792  xpord2ind  33794  xpord3lem  33795  frxp3  33797  xpord3pred  33798  naddcllem  33831  addsval  34126  brtxp  34182  brpprod  34187  brpprod3b  34189  brsset  34191  brtxpsd  34196  dffun10  34216  elfuns  34217  brcart  34234  brimg  34239  brapply  34240  brcup  34241  brcap  34242  brsuccf  34243  brrestrict  34251  dfrecs2  34252  dfrdg4  34253  fvtransport  34334  brcolinear2  34360  colineardim1  34363  brsegle  34410  fvline  34446  ellines  34454  filnetlem3  34569  bj-inftyexpitaufo  35373  bj-inftyexpitaudisj  35376  bj-inftyexpiinv  35379  bj-inftyexpidisj  35381  bj-elccinfty  35385  bj-minftyccb  35396  finxpreclem2  35561  finxp0  35562  finxp1o  35563  finxpreclem3  35564  finxpreclem4  35565  finxpreclem5  35566  finxpreclem6  35567  poimirlem9  35786  poimirlem15  35792  poimirlem17  35794  poimirlem20  35797  poimirlem24  35801  poimirlem28  35805  mblfinlem2  35815  heiborlem6  35974  heiborlem7  35975  heiborlem8  35976  grposnOLD  36040  rngosn3  36082  gidsn  36110  zrdivrng  36111  brxrn  36504  br1cossxrnres  36566  dvhvaddval  39104  dvhvscaval  39113  dibglbN  39180  dihglbcpreN  39314  dihmeetlem4preN  39320  dihmeetlem13N  39333  hdmapfval  39841  elcnvlem  41209  cotrintab  41222  elimaint  41257  snhesn  41394  projf1o  42736  dvnprodlem1  43487  dvnprodlem2  43488  sge0xp  43967  hoicvr  44086  hoicvrrex  44094  hoidmv1le  44132  hoi2toco  44145  ovnlecvr2  44148  ovolval5lem2  44191  fsetsnf1  44546  setsidel  44828  prproropf1olem3  44957  prproropf1olem4  44958  prproropreud  44961  ushrisomgr  45293  opeliun2xp  45668  lmod1lem2  45829  lmod1lem3  45830  lmod1zr  45834  zlmodzxznm  45838  zlmodzxzldeplem  45839  rrx2xpref1o  46064  line2x  46100  inlinecirc02plem  46132  thincciso  46330  mndtchom  46371