Theorem opex 5324

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 4757	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5301	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5177	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4470	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2848	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 399   ∈ wcel 2111  Vcvv 3409  ∅c0 4225  ifcif 4420  {csn 4522  {cpr 4524  ⟨cop 4528

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-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3861  df-un 3863  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529

This theorem is referenced by:  otex  5325  brv  5332  otth2  5343  otthg  5345  sbcop1  5347  oteqex2  5358  oteqex  5359  snopeqop  5365  propeqop  5366  propssopi  5367  euop2  5371  brsnop  5381  opabidw  5382  opabid  5383  elopab  5384  rexopabb  5385  opabn0  5410  opeliunxp  5588  elvvv  5596  opbrop  5617  relsnopg  5645  xpiindi  5675  raliunxp  5679  idrefALT  5945  intirr  5950  xpnz  5988  dmsnn0  6036  dmsnopg  6042  cnvcnvsn  6048  op2ndb  6056  opswap  6058  cnviin  6115  reuop  6122  funopg  6369  dffv2  6747  fsn  6888  f1o2sn  6895  idref  6899  funsndifnop  6904  fmptsng  6921  fmptsnd  6922  fvsng  6933  resfunexg  6969  fveqf1o  7051  fliftel  7056  fliftel1  7057  oprabidw  7181  oprabid  7182  dfoprab2  7206  oprabv  7208  rnoprab  7251  eloprabga  7255  ot1stg  7707  ot2ndg  7708  ot3rdg  7709  fo1st  7713  fo2nd  7714  br1steqg  7715  br2ndeqg  7716  opiota  7761  eloprabi  7765  mposn  7803  fpar  7816  fsplitfpar  7819  algrflem  7824  frxp  7825  xporderlem  7826  fnwelem  7830  fvproj  7833  fimaproj  7834  mpoxopoveq  7895  brtpos  7911  dmtpos  7914  rntpos  7915  tpostpos  7922  wfrlem14  7978  tfrlem11  8034  seqomlem1  8096  seqomlem3  8098  seqomlem4  8099  omeu  8221  iiner  8379  xpsnen  8622  xpcomco  8628  xpassen  8632  xpmapenlem  8706  dif1en  8733  unxpdomlem1  8760  inlresf  9376  inrresf  9378  djur  9381  djuss  9382  djuun  9388  1stinl  9389  2ndinl  9390  1stinr  9391  2ndinr  9392  fseqenlem2  9485  dju1dif  9632  fpwwe  10106  addpipq2  10396  addpqnq  10398  mulpipq2  10399  mulpqnq  10401  ordpipq  10402  prlem934  10493  addcnsr  10595  mulcnsr  10596  ltresr  10600  addcnsrec  10603  mulcnsrec  10604  axcnre  10624  om2uzrdg  13373  uzrdg0i  13376  uzrdgsuci  13377  hashfun  13848  wrdexb  13924  s1len  14007  s1nz  14008  s111  14016  wrdlen2i  14351  brintclab  14408  fsumcnv  15176  fprodcnv  15385  ruclem1  15632  ruclem4  15635  eucalgval2  15977  crth  16170  phimullem  16171  setsval  16571  setsdm  16575  setsfun  16576  setsfun0  16577  setsexstruct2  16580  setsres  16583  setscom  16585  strfv  16589  setsid  16596  imasaddfnlem  16859  imasaddvallem  16860  imasvscafn  16868  idfuval  17205  cofuval  17211  resfval  17221  resfval2  17222  elhoma  17358  embedsetcestrclem  17473  xpcco  17499  xpcid  17505  1stfval  17507  2ndfval  17510  prfval  17515  prf1  17516  prf2  17518  evlfval  17533  curfval  17539  curf1  17541  curfcl  17548  hofval  17568  intopsn  17930  mgm1  17934  sgrp1  17976  mnd1  18018  mnd1id  18019  grpss  18188  grp1  18273  symg2bas  18588  efgmval  18905  efgi  18912  efgi2  18918  frgpnabllem1  19061  frgpnabllem2  19062  ring1  19423  opsrtoslem2  20816  mat1dimelbas  21171  mat1dimbas  21172  mat1dimscm  21175  mat1dimmul  21176  mat1f1o  21178  mat1rhmelval  21180  mvmulfval  21242  m2detleib  21331  txcnp  22320  upxp  22323  uptx  22325  txdis1cn  22335  hauseqlcld  22346  txlm  22348  xkoinjcn  22387  txflf  22706  qustgplem  22821  ucnima  22982  ucnprima  22983  fmucndlem  22992  imasdsf1olem  23075  cnheiborlem  23655  ovollb2lem  24188  ovolctb  24190  ovolshftlem1  24209  ovolscalem1  24213  ovolicc1  24216  ioombl1lem3  24260  ioombl1lem4  24261  ioorval  24274  dyadval  24292  mbfimaopnlem  24355  limccnp2  24591  brbtwn  26792  brcgr  26793  eengbas  26874  ebtwntg  26875  ecgrtg  26876  elntg  26877  structvtxval  26913  structgrssvtx  26916  structgrssiedg  26917  gropd  26923  isuhgrop  26962  uhgrunop  26967  upgrop  26986  upgr0eop  27006  upgrunop  27011  umgrunop  27013  isuspgrop  27053  isusgrop  27054  ausgrusgrb  27057  usgr0eop  27135  usgrexmpl  27152  griedg0ssusgr  27154  uhgrspanop  27185  uhgrspan1  27192  upgrres  27195  umgrres  27196  usgrres  27197  upgrres1  27202  umgrres1  27203  usgrres1  27204  usgrexi  27330  cusgrexi  27332  cffldtocusgr  27336  cusgrres  27337  vtxdgop  27359  umgr2v2e  27414  wlkp1lem2  27563  wlkswwlksf1o  27764  wwlksnext  27778  eupth2eucrct  28101  eupthvdres  28119  konigsbergumgr  28135  numclwwlk1lem2fv  28240  numclwlk1lem1  28253  ex-br  28315  ex-fpar  28346  cnnvg  28560  cnnvs  28562  cnnvnm  28563  h2hva  28856  h2hsm  28857  h2hnm  28858  hhssva  29139  hhsssm  29140  hhssnm  29141  hhshsslem1  29149  br8d  30472  xppreima2  30511  aciunf1lem  30523  ofpreima  30526  cnvoprabOLD  30579  linds2eq  31096  smatrcl  31267  smatlem  31268  txomap  31305  qtophaus  31307  hgt750lemb  32155  bnj97  32366  bnj553  32398  bnj966  32444  bnj1442  32549  erdszelem9  32677  erdszelem10  32678  txpconn  32710  txsconnlem  32718  goel  32825  goeleq12bg  32827  gonafv  32828  gonanegoal  32830  sat1el2xp  32857  fmlaomn0  32868  gonan0  32870  goaln0  32871  gonarlem  32872  gonar  32873  goalrlem  32874  goalr  32875  fmla0disjsuc  32876  fmlasucdisj  32877  satffunlem  32879  satffunlem1lem1  32880  satffunlem2lem1  32882  satfv0fvfmla0  32891  sategoelfvb  32897  prv1n  32909  msubval  33003  mvhval  33012  msubvrs  33038  brtpid1  33183  brtpid2  33184  brtpid3  33185  ot21std  33199  ot22ndd  33200  otthne  33201  ralxp3f  33204  sbcoteq1a  33206  brtp  33232  dfpo2  33238  br8  33239  br6  33240  br4  33241  dfdm5  33263  dfrn5  33264  elima4  33266  fv1stcnv  33267  fv2ndcnv  33268  xpord2lem  33344  xpord2pred  33347  xpord2ind  33349  xpord3lem  33350  frxp3  33352  xpord3pred  33353  no3indslem  33662  addsov  33674  brtxp  33731  brpprod  33736  brpprod3b  33738  brsset  33740  brtxpsd  33745  dffun10  33765  elfuns  33766  brcart  33783  brimg  33788  brapply  33789  brcup  33790  brcap  33791  brsuccf  33792  brrestrict  33800  dfrecs2  33801  dfrdg4  33802  fvtransport  33883  brcolinear2  33909  colineardim1  33912  brsegle  33959  fvline  33995  ellines  34003  filnetlem3  34118  bj-inftyexpitaufo  34897  bj-inftyexpitaudisj  34900  bj-inftyexpiinv  34903  bj-inftyexpidisj  34905  bj-elccinfty  34909  bj-minftyccb  34920  finxpreclem2  35087  finxp0  35088  finxp1o  35089  finxpreclem3  35090  finxpreclem4  35091  finxpreclem5  35092  finxpreclem6  35093  poimirlem9  35346  poimirlem15  35352  poimirlem17  35354  poimirlem20  35357  poimirlem24  35361  poimirlem28  35365  mblfinlem2  35375  heiborlem6  35534  heiborlem7  35535  heiborlem8  35536  grposnOLD  35600  rngosn3  35642  gidsn  35670  zrdivrng  35671  brxrn  36066  br1cossxrnres  36128  dvhvaddval  38666  dvhvscaval  38675  dibglbN  38742  dihglbcpreN  38876  dihmeetlem4preN  38882  dihmeetlem13N  38895  hdmapfval  39403  elcnvlem  40674  cotrintab  40687  elimaint  40722  snhesn  40860  projf1o  42195  dvnprodlem1  42954  dvnprodlem2  42955  sge0xp  43434  hoicvr  43553  hoicvrrex  43561  hoidmv1le  43599  hoi2toco  43612  ovnlecvr2  43615  ovolval5lem2  43658  setsidel  44261  prproropf1olem3  44390  prproropf1olem4  44391  prproropreud  44394  ushrisomgr  44726  opeliun2xp  45101  lmod1lem2  45262  lmod1lem3  45263  lmod1zr  45267  zlmodzxznm  45271  zlmodzxzldeplem  45272  rrx2xpref1o  45497  line2x  45533  inlinecirc02plem  45565