Theorem opex 5484

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 4894	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5452	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5325	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4598	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2840	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  ifcif 4548  {csn 4648  {cpr 4650  ⟨cop 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655

This theorem is referenced by:  otex  5485  brv  5492  otth2  5503  otthg  5505  sbcop1  5508  oteqex2  5518  oteqex  5519  snopeqop  5525  propeqop  5526  propssopi  5527  euop2  5531  brsnop  5541  brtp  5542  opabidw  5543  opabid  5544  elopab  5546  rexopabb  5547  opabn0  5572  opeliunxp  5767  elvvv  5775  opbrop  5797  relsnopg  5827  xpiindi  5860  raliunxp  5864  idrefALT  6143  intirr  6150  xpnz  6190  dmsnn0  6238  dmsnopg  6244  cnvcnvsn  6250  op2ndb  6258  opswap  6260  cnviin  6317  reuop  6324  dfpo2  6327  funopg  6612  dffv2  7017  fsn  7169  f1o2sn  7176  idref  7180  funsndifnop  7185  fmptsng  7202  fmptsnd  7203  fvsng  7214  resfunexg  7252  fveqf1o  7338  fliftel  7345  fliftel1  7346  oprabidw  7479  oprabid  7480  dfoprab2  7508  oprabv  7510  rnoprab  7554  eloprabga  7558  eloprabgaOLD  7559  ot1stg  8044  ot2ndg  8045  ot3rdg  8046  fo1st  8050  fo2nd  8051  br1steqg  8052  br2ndeqg  8053  opiota  8100  eloprabi  8104  mposn  8144  fpar  8157  fsplitfpar  8159  opco1  8164  opco2  8165  frxp  8167  xporderlem  8168  fnwelem  8172  fvproj  8175  fimaproj  8176  xpord2lem  8183  xpord2pred  8186  xpord2indlem  8188  frxp3  8192  mpoxopoveq  8260  brtpos  8276  dmtpos  8279  rntpos  8280  tpostpos  8287  wfrlem14OLD  8378  tfrlem11  8444  seqomlem1  8506  seqomlem3  8508  seqomlem4  8509  omeu  8641  naddcllem  8732  iiner  8847  xpsnen  9121  xpcomco  9128  xpassen  9132  xpmapenlem  9210  dif1en  9226  dif1enOLD  9228  unxpdomlem1  9313  inlresf  9983  inrresf  9985  djur  9988  djuss  9989  djuun  9995  1stinl  9996  2ndinl  9997  1stinr  9998  2ndinr  9999  fseqenlem2  10094  dju1dif  10242  fpwwe  10715  addpipq2  11005  addpqnq  11007  mulpipq2  11008  mulpqnq  11010  ordpipq  11011  prlem934  11102  addcnsr  11204  mulcnsr  11205  ltresr  11209  addcnsrec  11212  mulcnsrec  11213  axcnre  11233  om2uzrdg  14007  uzrdg0i  14010  uzrdgsuci  14011  hashfun  14486  wrdexb  14573  s1len  14654  s1nz  14655  s111  14663  wrdlen2i  14991  brintclab  15050  fsumcnv  15821  fprodcnv  16031  ruclem1  16279  ruclem4  16282  eucalgval2  16628  crth  16825  phimullem  16826  setsval  17214  setsdm  17217  setsfun  17218  setsfun0  17219  setsexstruct2  17222  setsres  17225  setscom  17227  strfv  17251  setsid  17255  imasaddfnlem  17588  imasaddvallem  17589  imasvscafn  17597  idfuval  17940  cofuval  17946  resfval  17956  resfval2  17957  elhoma  18099  embedsetcestrclem  18226  xpcco  18252  xpcid  18258  1stfval  18260  2ndfval  18263  prfval  18268  prf1  18269  prf2  18271  evlfval  18287  curfval  18293  curf1  18295  curfcl  18302  hofval  18322  intopsn  18692  mgm1  18696  sgrp1  18767  mnd1  18814  mnd1id  18815  grpss  18994  grp1  19087  symg2bas  19434  efgmval  19754  efgi  19761  efgi2  19767  frgpnabllem1  19915  frgpnabllem2  19916  ring1  20333  rngqiprngimfv  21331  rngqiprngimf1  21333  opsrtoslem2  22103  mat1dimelbas  22498  mat1dimbas  22499  mat1dimscm  22502  mat1dimmul  22503  mat1f1o  22505  mat1rhmelval  22507  mvmulfval  22569  m2detleib  22658  txcnp  23649  upxp  23652  uptx  23654  txdis1cn  23664  hauseqlcld  23675  txlm  23677  xkoinjcn  23716  txflf  24035  qustgplem  24150  ucnima  24311  ucnprima  24312  fmucndlem  24321  imasdsf1olem  24404  cnheiborlem  25005  ovollb2lem  25542  ovolctb  25544  ovolshftlem1  25563  ovolscalem1  25567  ovolicc1  25570  ioombl1lem3  25614  ioombl1lem4  25615  ioorval  25628  dyadval  25646  mbfimaopnlem  25709  limccnp2  25947  addsval  28013  mulsval  28153  precsexlem1  28249  precsexlem2  28250  precsexlem3  28251  om2noseqrdg  28328  noseqrdg0  28331  noseqrdgsuc  28332  brbtwn  28932  brcgr  28933  eengbas  29014  ebtwntg  29015  ecgrtg  29016  elntg  29017  structvtxval  29056  structgrssvtx  29059  structgrssiedg  29060  gropd  29066  isuhgrop  29105  uhgrunop  29110  upgrop  29129  upgr0eop  29149  upgrunop  29154  umgrunop  29156  isuspgrop  29196  isusgrop  29197  ausgrusgrb  29200  usgr0eop  29281  griedg0ssusgr  29300  uhgrspanop  29331  uhgrspan1  29338  upgrres  29341  umgrres  29342  usgrres  29343  upgrres1  29348  umgrres1  29349  usgrres1  29350  usgrexi  29476  cusgrexi  29478  cffldtocusgr  29482  cffldtocusgrOLD  29483  cusgrres  29484  vtxdgop  29506  umgr2v2e  29561  wlkp1lem2  29710  wlkswwlksf1o  29912  wwlksnext  29926  eupth2eucrct  30249  eupthvdres  30267  konigsbergumgr  30283  numclwwlk1lem2fv  30388  numclwlk1lem1  30401  ex-br  30463  ex-fpar  30494  cnnvg  30710  cnnvs  30712  cnnvnm  30713  h2hva  31006  h2hsm  31007  h2hnm  31008  hhssva  31289  hhsssm  31290  hhssnm  31291  hhshsslem1  31299  br8d  32632  xppreima2  32669  aciunf1lem  32680  ofpreima  32683  cnvoprabOLD  32734  rlocaddval  33240  rlocmulval  33241  linds2eq  33374  smatrcl  33742  smatlem  33743  txomap  33780  qtophaus  33782  hgt750lemb  34633  bnj97  34842  bnj553  34874  bnj966  34920  bnj1442  35025  erdszelem9  35167  erdszelem10  35168  txpconn  35200  txsconnlem  35208  goel  35315  goeleq12bg  35317  gonafv  35318  gonanegoal  35320  sat1el2xp  35347  fmlaomn0  35358  gonan0  35360  goaln0  35361  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  fmla0disjsuc  35366  fmlasucdisj  35367  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  satfv0fvfmla0  35381  sategoelfvb  35387  prv1n  35399  msubval  35493  mvhval  35502  msubvrs  35528  brtpid1  35683  brtpid2  35684  brtpid3  35685  br8  35718  br6  35719  br4  35720  dfdm5  35736  dfrn5  35737  elima4  35739  fv1stcnv  35740  fv2ndcnv  35741  brtxp  35844  brpprod  35849  brpprod3b  35851  brsset  35853  brtxpsd  35858  dffun10  35878  elfuns  35879  brcart  35896  brimg  35901  brapply  35902  brcup  35903  brcap  35904  brsuccf  35905  brrestrict  35913  dfrecs2  35914  dfrdg4  35915  fvtransport  35996  brcolinear2  36022  colineardim1  36025  brsegle  36072  fvline  36108  ellines  36116  filnetlem3  36346  bj-inftyexpitaufo  37168  bj-inftyexpitaudisj  37171  bj-inftyexpiinv  37174  bj-inftyexpidisj  37176  bj-elccinfty  37180  bj-minftyccb  37191  finxpreclem2  37356  finxp0  37357  finxp1o  37358  finxpreclem3  37359  finxpreclem4  37360  finxpreclem5  37361  finxpreclem6  37362  poimirlem9  37589  poimirlem15  37595  poimirlem17  37597  poimirlem20  37600  poimirlem24  37604  poimirlem28  37608  mblfinlem2  37618  heiborlem6  37776  heiborlem7  37777  heiborlem8  37778  grposnOLD  37842  rngosn3  37884  gidsn  37912  zrdivrng  37913  brxrn  38330  br1cossxrnres  38404  dvhvaddval  41047  dvhvscaval  41056  dibglbN  41123  dihglbcpreN  41257  dihmeetlem4preN  41263  dihmeetlem13N  41276  hdmapfval  41784  elcnvlem  43563  cotrintab  43576  elimaint  43611  snhesn  43748  projf1o  45104  dvnprodlem1  45867  dvnprodlem2  45868  sge0xp  46350  hoicvr  46469  hoicvrrex  46477  hoidmv1le  46515  hoi2toco  46528  ovnlecvr2  46531  ovolval5lem2  46574  fsetsnf1  46967  setsidel  47250  prproropf1olem3  47379  prproropf1olem4  47380  prproropreud  47383  isisubgr  47734  ushggricedg  47780  opeliun2xp  48057  lmod1lem2  48217  lmod1lem3  48218  lmod1zr  48222  zlmodzxznm  48226  zlmodzxzldeplem  48227  rrx2xpref1o  48452  line2x  48488  inlinecirc02plem  48520  thincciso  48716  mndtchom  48757