Theorem opex 5426

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 4832	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5394	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5269	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4541	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2828	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 396   ∈ wcel 2106  Vcvv 3446  ∅c0 4287  ifcif 4491  {csn 4591  {cpr 4593  ⟨cop 4597

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598

This theorem is referenced by:  otex  5427  brv  5434  otth2  5445  otthg  5447  sbcop1  5450  oteqex2  5461  oteqex  5462  snopeqop  5468  propeqop  5469  propssopi  5470  euop2  5474  brsnop  5484  brtp  5485  opabidw  5486  opabid  5487  elopab  5489  rexopabb  5490  opabn0  5515  opeliunxp  5704  elvvv  5712  opbrop  5734  relsnopg  5764  xpiindi  5796  raliunxp  5800  idrefALT  6070  intirr  6077  xpnz  6116  dmsnn0  6164  dmsnopg  6170  cnvcnvsn  6176  op2ndb  6184  opswap  6186  cnviin  6243  reuop  6250  dfpo2  6253  funopg  6540  dffv2  6941  fsn  7086  f1o2sn  7093  idref  7097  funsndifnop  7102  fmptsng  7119  fmptsnd  7120  fvsng  7131  resfunexg  7170  fveqf1o  7254  fliftel  7259  fliftel1  7260  oprabidw  7393  oprabid  7394  dfoprab2  7420  oprabv  7422  rnoprab  7465  eloprabga  7469  eloprabgaOLD  7470  ot1stg  7940  ot2ndg  7941  ot3rdg  7942  fo1st  7946  fo2nd  7947  br1steqg  7948  br2ndeqg  7949  opiota  7996  eloprabi  8000  mposn  8040  fpar  8053  fsplitfpar  8055  opco1  8060  opco2  8061  frxp  8063  xporderlem  8064  fnwelem  8068  fvproj  8071  fimaproj  8072  xpord2lem  8079  xpord2pred  8082  xpord2indlem  8084  frxp3  8088  mpoxopoveq  8155  brtpos  8171  dmtpos  8174  rntpos  8175  tpostpos  8182  wfrlem14OLD  8273  tfrlem11  8339  seqomlem1  8401  seqomlem3  8403  seqomlem4  8404  omeu  8537  naddcllem  8627  iiner  8735  xpsnen  9006  xpcomco  9013  xpassen  9017  xpmapenlem  9095  dif1en  9111  dif1enOLD  9113  unxpdomlem1  9201  inlresf  9859  inrresf  9861  djur  9864  djuss  9865  djuun  9871  1stinl  9872  2ndinl  9873  1stinr  9874  2ndinr  9875  fseqenlem2  9970  dju1dif  10117  fpwwe  10591  addpipq2  10881  addpqnq  10883  mulpipq2  10884  mulpqnq  10886  ordpipq  10887  prlem934  10978  addcnsr  11080  mulcnsr  11081  ltresr  11085  addcnsrec  11088  mulcnsrec  11089  axcnre  11109  om2uzrdg  13871  uzrdg0i  13874  uzrdgsuci  13875  hashfun  14347  wrdexb  14425  s1len  14506  s1nz  14507  s111  14515  wrdlen2i  14843  brintclab  14898  fsumcnv  15669  fprodcnv  15877  ruclem1  16124  ruclem4  16127  eucalgval2  16468  crth  16661  phimullem  16662  setsval  17050  setsdm  17053  setsfun  17054  setsfun0  17055  setsexstruct2  17058  setsres  17061  setscom  17063  strfv  17087  setsid  17091  imasaddfnlem  17424  imasaddvallem  17425  imasvscafn  17433  idfuval  17776  cofuval  17782  resfval  17792  resfval2  17793  elhoma  17932  embedsetcestrclem  18059  xpcco  18085  xpcid  18091  1stfval  18093  2ndfval  18096  prfval  18101  prf1  18102  prf2  18104  evlfval  18120  curfval  18126  curf1  18128  curfcl  18135  hofval  18155  intopsn  18523  mgm1  18527  sgrp1  18569  mnd1  18611  mnd1id  18612  grpss  18782  grp1  18868  symg2bas  19188  efgmval  19508  efgi  19515  efgi2  19521  frgpnabllem1  19665  frgpnabllem2  19666  ring1  20040  opsrtoslem2  21500  mat1dimelbas  21857  mat1dimbas  21858  mat1dimscm  21861  mat1dimmul  21862  mat1f1o  21864  mat1rhmelval  21866  mvmulfval  21928  m2detleib  22017  txcnp  23008  upxp  23011  uptx  23013  txdis1cn  23023  hauseqlcld  23034  txlm  23036  xkoinjcn  23075  txflf  23394  qustgplem  23509  ucnima  23670  ucnprima  23671  fmucndlem  23680  imasdsf1olem  23763  cnheiborlem  24354  ovollb2lem  24889  ovolctb  24891  ovolshftlem1  24910  ovolscalem1  24914  ovolicc1  24917  ioombl1lem3  24961  ioombl1lem4  24962  ioorval  24975  dyadval  24993  mbfimaopnlem  25056  limccnp2  25293  addsval  27317  mulsval  27417  brbtwn  27911  brcgr  27912  eengbas  27993  ebtwntg  27994  ecgrtg  27995  elntg  27996  structvtxval  28035  structgrssvtx  28038  structgrssiedg  28039  gropd  28045  isuhgrop  28084  uhgrunop  28089  upgrop  28108  upgr0eop  28128  upgrunop  28133  umgrunop  28135  isuspgrop  28175  isusgrop  28176  ausgrusgrb  28179  usgr0eop  28257  usgrexmpl  28274  griedg0ssusgr  28276  uhgrspanop  28307  uhgrspan1  28314  upgrres  28317  umgrres  28318  usgrres  28319  upgrres1  28324  umgrres1  28325  usgrres1  28326  usgrexi  28452  cusgrexi  28454  cffldtocusgr  28458  cusgrres  28459  vtxdgop  28481  umgr2v2e  28536  wlkp1lem2  28685  wlkswwlksf1o  28887  wwlksnext  28901  eupth2eucrct  29224  eupthvdres  29242  konigsbergumgr  29258  numclwwlk1lem2fv  29363  numclwlk1lem1  29376  ex-br  29438  ex-fpar  29469  cnnvg  29683  cnnvs  29685  cnnvnm  29686  h2hva  29979  h2hsm  29980  h2hnm  29981  hhssva  30262  hhsssm  30263  hhssnm  30264  hhshsslem1  30272  br8d  31596  xppreima2  31634  aciunf1lem  31645  ofpreima  31648  cnvoprabOLD  31705  linds2eq  32241  smatrcl  32466  smatlem  32467  txomap  32504  qtophaus  32506  hgt750lemb  33358  bnj97  33567  bnj553  33599  bnj966  33645  bnj1442  33750  erdszelem9  33880  erdszelem10  33881  txpconn  33913  txsconnlem  33921  goel  34028  goeleq12bg  34030  gonafv  34031  gonanegoal  34033  sat1el2xp  34060  fmlaomn0  34071  gonan0  34073  goaln0  34074  gonarlem  34075  gonar  34076  goalrlem  34077  goalr  34078  fmla0disjsuc  34079  fmlasucdisj  34080  satffunlem  34082  satffunlem1lem1  34083  satffunlem2lem1  34085  satfv0fvfmla0  34094  sategoelfvb  34100  prv1n  34112  msubval  34206  mvhval  34215  msubvrs  34241  brtpid1  34379  brtpid2  34380  brtpid3  34381  br8  34415  br6  34416  br4  34417  dfdm5  34433  dfrn5  34434  elima4  34436  fv1stcnv  34437  fv2ndcnv  34438  brtxp  34541  brpprod  34546  brpprod3b  34548  brsset  34550  brtxpsd  34555  dffun10  34575  elfuns  34576  brcart  34593  brimg  34598  brapply  34599  brcup  34600  brcap  34601  brsuccf  34602  brrestrict  34610  dfrecs2  34611  dfrdg4  34612  fvtransport  34693  brcolinear2  34719  colineardim1  34722  brsegle  34769  fvline  34805  ellines  34813  filnetlem3  34928  bj-inftyexpitaufo  35746  bj-inftyexpitaudisj  35749  bj-inftyexpiinv  35752  bj-inftyexpidisj  35754  bj-elccinfty  35758  bj-minftyccb  35769  finxpreclem2  35934  finxp0  35935  finxp1o  35936  finxpreclem3  35937  finxpreclem4  35938  finxpreclem5  35939  finxpreclem6  35940  poimirlem9  36160  poimirlem15  36166  poimirlem17  36168  poimirlem20  36171  poimirlem24  36175  poimirlem28  36179  mblfinlem2  36189  heiborlem6  36348  heiborlem7  36349  heiborlem8  36350  grposnOLD  36414  rngosn3  36456  gidsn  36484  zrdivrng  36485  brxrn  36909  br1cossxrnres  36983  dvhvaddval  39626  dvhvscaval  39635  dibglbN  39702  dihglbcpreN  39836  dihmeetlem4preN  39842  dihmeetlem13N  39855  hdmapfval  40363  elcnvlem  41995  cotrintab  42008  elimaint  42043  snhesn  42180  projf1o  43539  dvnprodlem1  44307  dvnprodlem2  44308  sge0xp  44790  hoicvr  44909  hoicvrrex  44917  hoidmv1le  44955  hoi2toco  44968  ovnlecvr2  44971  ovolval5lem2  45014  fsetsnf1  45406  setsidel  45688  prproropf1olem3  45817  prproropf1olem4  45818  prproropreud  45821  ushrisomgr  46153  opeliun2xp  46528  lmod1lem2  46689  lmod1lem3  46690  lmod1zr  46694  zlmodzxznm  46698  zlmodzxzldeplem  46699  rrx2xpref1o  46924  line2x  46960  inlinecirc02plem  46992  thincciso  47189  mndtchom  47230