Theorem opex 5321

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 4760	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5298	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5175	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4473	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2886	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 399   ∈ wcel 2111  Vcvv 3441  ∅c0 4243  ifcif 4425  {csn 4525  {cpr 4527  ⟨cop 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532

This theorem is referenced by:  otex  5322  brv  5329  otth2  5340  otthg  5342  sbcop1  5344  oteqex2  5354  oteqex  5355  snopeqop  5361  propeqop  5362  propssopi  5363  euop2  5367  opabidw  5377  opabid  5378  elopab  5379  rexopabb  5380  opabn0  5405  opeliunxp  5583  elvvv  5591  opbrop  5612  relsnopg  5640  xpiindi  5670  raliunxp  5674  idrefALT  5940  intirr  5945  xpnz  5983  dmsnn0  6031  dmsnopg  6037  cnvcnvsn  6043  op2ndb  6051  opswap  6053  cnviin  6105  reuop  6112  funopg  6358  dffv2  6733  fsn  6874  f1o2sn  6881  idref  6885  funsndifnop  6890  fmptsng  6907  fmptsnd  6908  fvsng  6919  resfunexg  6955  fveqf1o  7037  fliftel  7041  fliftel1  7042  oprabidw  7166  oprabid  7167  dfoprab2  7191  oprabv  7193  rnoprab  7236  eloprabga  7240  ot1stg  7685  ot2ndg  7686  ot3rdg  7687  fo1st  7691  fo2nd  7692  br1steqg  7693  br2ndeqg  7694  opiota  7739  eloprabi  7743  mposn  7781  fpar  7794  fsplitfpar  7797  algrflem  7802  frxp  7803  xporderlem  7804  fnwelem  7808  fvproj  7811  fimaproj  7812  mpoxopoveq  7868  brtpos  7884  dmtpos  7887  rntpos  7888  tpostpos  7895  wfrlem14  7951  tfrlem11  8007  seqomlem1  8069  seqomlem3  8071  seqomlem4  8072  omeu  8194  iiner  8352  xpsnen  8584  xpcomco  8590  xpassen  8594  xpmapenlem  8668  unxpdomlem1  8706  inlresf  9327  inrresf  9329  djur  9332  djuss  9333  djuun  9339  1stinl  9340  2ndinl  9341  1stinr  9342  2ndinr  9343  fseqenlem2  9436  dju1dif  9583  fpwwe  10057  addpipq2  10347  addpqnq  10349  mulpipq2  10350  mulpqnq  10352  ordpipq  10353  prlem934  10444  addcnsr  10546  mulcnsr  10547  ltresr  10551  addcnsrec  10554  mulcnsrec  10555  axcnre  10575  om2uzrdg  13319  uzrdg0i  13322  uzrdgsuci  13323  hashfun  13794  wrdexb  13868  s1len  13951  s1nz  13952  s111  13960  wrdlen2i  14295  brintclab  14352  fsumcnv  15120  fprodcnv  15329  ruclem1  15576  ruclem4  15579  eucalgval2  15915  crth  16105  phimullem  16106  setsval  16505  setsdm  16509  setsfun  16510  setsfun0  16511  setsexstruct2  16514  setsres  16517  setscom  16519  strfv  16523  setsid  16530  imasaddfnlem  16793  imasaddvallem  16794  imasvscafn  16802  idfuval  17138  cofuval  17144  resfval  17154  resfval2  17155  elhoma  17284  embedsetcestrclem  17399  xpcco  17425  xpcid  17431  1stfval  17433  2ndfval  17436  prfval  17441  prf1  17442  prf2  17444  evlfval  17459  curfval  17465  curf1  17467  curfcl  17474  hofval  17494  intopsn  17856  mgm1  17860  sgrp1  17902  mnd1  17944  mnd1id  17945  grpss  18113  grp1  18198  symg2bas  18513  efgmval  18830  efgi  18837  efgi2  18843  frgpnabllem1  18986  frgpnabllem2  18987  ring1  19348  opsrtoslem2  20724  mat1dimelbas  21076  mat1dimbas  21077  mat1dimscm  21080  mat1dimmul  21081  mat1f1o  21083  mat1rhmelval  21085  mvmulfval  21147  m2detleib  21236  txcnp  22225  upxp  22228  uptx  22230  txdis1cn  22240  hauseqlcld  22251  txlm  22253  xkoinjcn  22292  txflf  22611  qustgplem  22726  ucnima  22887  ucnprima  22888  fmucndlem  22897  imasdsf1olem  22980  cnheiborlem  23559  ovollb2lem  24092  ovolctb  24094  ovolshftlem1  24113  ovolscalem1  24117  ovolicc1  24120  ioombl1lem3  24164  ioombl1lem4  24165  ioorval  24178  dyadval  24196  mbfimaopnlem  24259  limccnp2  24495  brbtwn  26693  brcgr  26694  eengbas  26775  ebtwntg  26776  ecgrtg  26777  elntg  26778  structvtxval  26814  structgrssvtx  26817  structgrssiedg  26818  gropd  26824  isuhgrop  26863  uhgrunop  26868  upgrop  26887  upgr0eop  26907  upgrunop  26912  umgrunop  26914  isuspgrop  26954  isusgrop  26955  ausgrusgrb  26958  usgr0eop  27036  usgrexmpl  27053  griedg0ssusgr  27055  uhgrspanop  27086  uhgrspan1  27093  upgrres  27096  umgrres  27097  usgrres  27098  upgrres1  27103  umgrres1  27104  usgrres1  27105  usgrexi  27231  cusgrexi  27233  cffldtocusgr  27237  cusgrres  27238  vtxdgop  27260  umgr2v2e  27315  wlkp1lem2  27464  wlkswwlksf1o  27665  wwlksnext  27679  eupth2eucrct  28002  eupthvdres  28020  konigsbergumgr  28036  numclwwlk1lem2fv  28141  numclwlk1lem1  28154  ex-br  28216  ex-fpar  28247  cnnvg  28461  cnnvs  28463  cnnvnm  28464  h2hva  28757  h2hsm  28758  h2hnm  28759  hhssva  29040  hhsssm  29041  hhssnm  29042  hhshsslem1  29050  br8d  30374  xppreima2  30413  aciunf1lem  30425  ofpreima  30428  brsnop  30453  cnvoprabOLD  30482  linds2eq  30995  smatrcl  31149  smatlem  31150  txomap  31187  qtophaus  31189  hgt750lemb  32037  bnj97  32248  bnj553  32280  bnj966  32326  bnj1442  32431  erdszelem9  32559  erdszelem10  32560  txpconn  32592  txsconnlem  32600  goel  32707  goeleq12bg  32709  gonafv  32710  gonanegoal  32712  sat1el2xp  32739  fmlaomn0  32750  gonan0  32752  goaln0  32753  gonarlem  32754  gonar  32755  goalrlem  32756  goalr  32757  fmla0disjsuc  32758  fmlasucdisj  32759  satffunlem  32761  satffunlem1lem1  32762  satffunlem2lem1  32764  satfv0fvfmla0  32773  sategoelfvb  32779  prv1n  32791  msubval  32885  mvhval  32894  msubvrs  32920  brtpid1  33064  brtpid2  33065  brtpid3  33066  brtp  33098  dfpo2  33104  br8  33105  br6  33106  br4  33107  dfdm5  33129  dfrn5  33130  elima4  33132  fv1stcnv  33133  fv2ndcnv  33134  brtxp  33454  brpprod  33459  brpprod3b  33461  brsset  33463  brtxpsd  33468  dffun10  33488  elfuns  33489  brcart  33506  brimg  33511  brapply  33512  brcup  33513  brcap  33514  brsuccf  33515  brrestrict  33523  dfrecs2  33524  dfrdg4  33525  fvtransport  33606  brcolinear2  33632  colineardim1  33635  brsegle  33682  fvline  33718  ellines  33726  filnetlem3  33841  bj-inftyexpitaufo  34617  bj-inftyexpitaudisj  34620  bj-inftyexpiinv  34623  bj-inftyexpidisj  34625  bj-elccinfty  34629  bj-minftyccb  34640  finxpreclem2  34807  finxp0  34808  finxp1o  34809  finxpreclem3  34810  finxpreclem4  34811  finxpreclem5  34812  finxpreclem6  34813  poimirlem9  35066  poimirlem15  35072  poimirlem17  35074  poimirlem20  35077  poimirlem24  35081  poimirlem28  35085  mblfinlem2  35095  heiborlem6  35254  heiborlem7  35255  heiborlem8  35256  grposnOLD  35320  rngosn3  35362  gidsn  35390  zrdivrng  35391  brxrn  35786  br1cossxrnres  35848  dvhvaddval  38386  dvhvscaval  38395  dibglbN  38462  dihglbcpreN  38596  dihmeetlem4preN  38602  dihmeetlem13N  38615  hdmapfval  39123  elcnvlem  40301  cotrintab  40314  elimaint  40349  snhesn  40487  projf1o  41825  dvnprodlem1  42588  dvnprodlem2  42589  sge0xp  43068  hoicvr  43187  hoicvrrex  43195  hoidmv1le  43233  hoi2toco  43246  ovnlecvr2  43249  ovolval5lem2  43292  setsidel  43893  prproropf1olem3  44022  prproropf1olem4  44023  prproropreud  44026  ushrisomgr  44359  opeliun2xp  44734  lmod1lem2  44897  lmod1lem3  44898  lmod1zr  44902  zlmodzxznm  44906  zlmodzxzldeplem  44907  rrx2xpref1o  45132  line2x  45168  inlinecirc02plem  45200