Theorem opex 4932

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 4399	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 4909	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 4790	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4156	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2697	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 384   ∈ wcel 1990  Vcvv 3200  ∅c0 3915  ifcif 4086  {csn 4177  {cpr 4179  ⟨cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  otex  4933  brv  4941  otth2  4952  otthg  4954  oteqex2  4963  oteqex  4964  snopeqop  4969  propeqop  4970  propssopi  4971  euop2  4974  opabid  4982  elopab  4983  opabn0  5006  opeliunxp  5170  elvvv  5178  opbrop  5198  relsnop  5224  xpiindi  5257  raliunxp  5261  intirr  5514  xpnz  5553  dmsnn0  5600  dmsnopg  5606  cnvcnvsn  5612  op2ndb  5619  opswap  5622  cnviin  5672  funopg  5922  dffv2  6271  fsn  6402  f1o2sn  6408  funsndifnop  6416  fmptsng  6434  fmptsnd  6435  fvsn  6446  fpr2g  6475  resfunexg  6479  idref  6499  fveqf1o  6557  fliftel  6559  fliftel1  6560  oprabid  6677  dfoprab2  6701  oprabv  6703  rnoprab  6743  eloprabga  6747  ot1stg  7182  ot2ndg  7183  ot3rdg  7184  fo1st  7188  fo2nd  7189  opiota  7229  eloprabi  7232  mpt2sn  7268  fpar  7281  algrflem  7286  frxp  7287  xporderlem  7288  fnwelem  7292  mpt2xopoveq  7345  brtpos  7361  dmtpos  7364  rntpos  7365  tpostpos  7372  wfrlem14  7428  tfrlem11  7484  seqomlem1  7545  seqomlem3  7547  seqomlem4  7548  omeu  7665  iiner  7819  xpsnen  8044  xpcomco  8050  xpassen  8054  xpmapenlem  8127  unxpdomlem1  8164  fseqenlem2  8848  cda1dif  8998  fpwwe  9468  addpipq2  9758  addpqnq  9760  mulpipq2  9761  mulpqnq  9763  ordpipq  9764  prlem934  9855  addcnsr  9956  mulcnsr  9957  ltresr  9961  addcnsrec  9964  mulcnsrec  9965  axcnre  9985  om2uzrdg  12755  uzrdg0i  12758  uzrdgsuci  12759  hashfun  13224  wrdexb  13316  s1len  13385  s1nz  13386  s111  13395  wrdlen2i  13686  brintclab  13742  fsumcnv  14504  fprodcnv  14713  ruclem1  14960  ruclem4  14963  eucalgval2  15294  crth  15483  phimullem  15484  setsval  15888  setsdm  15892  setsfun  15893  setsfun0  15894  setsexstruct2  15897  setsres  15901  setscom  15903  strfv  15907  setsid  15914  imasaddfnlem  16188  imasaddvallem  16189  imasvscafn  16197  idfuval  16536  cofuval  16542  resfval  16552  resfval2  16553  elhoma  16682  embedsetcestrclem  16797  xpcco  16823  xpcid  16829  1stfval  16831  2ndfval  16834  prfval  16839  prf1  16840  prf2  16842  evlfval  16857  curfval  16863  curf1  16865  curfcl  16872  hofval  16892  intopsn  17253  mgm1  17257  sgrp1  17293  mnd1  17331  mnd1id  17332  grpss  17440  grp1  17522  symg2bas  17818  efgmval  18125  efgi  18132  efgi2  18138  frgpnabllem1  18276  frgpnabllem2  18277  ring1  18602  opsrtoslem2  19485  mat1dimelbas  20277  mat1dimbas  20278  mat1dimscm  20281  mat1dimmul  20282  mat1f1o  20284  mat1rhmelval  20286  mvmulfval  20348  m2detleib  20437  txcnp  21423  upxp  21426  uptx  21428  txdis1cn  21438  hauseqlcld  21449  txlm  21451  xkoinjcn  21490  txflf  21810  qustgplem  21924  ucnima  22085  ucnprima  22086  fmucndlem  22095  imasdsf1olem  22178  cnheiborlem  22753  ovollb2lem  23256  ovolctb  23258  ovolshftlem1  23277  ovolscalem1  23281  ovolicc1  23284  ioombl1lem3  23328  ioombl1lem4  23329  ioorval  23342  dyadval  23360  mbfimaopnlem  23422  limccnp2  23656  brbtwn  25779  brcgr  25780  eengbas  25861  ebtwntg  25862  ecgrtg  25863  elntg  25864  structvtxval  25910  structgrssvtx  25913  structgrssiedg  25914  structgrssvtxOLD  25916  structgrssiedgOLD  25917  gropd  25923  isuhgrop  25965  uhgrunop  25970  upgrop  25989  upgr0eop  26009  upgrunop  26014  umgrunop  26016  isuspgrop  26056  isusgrop  26057  ausgrusgrb  26060  usgr0eop  26138  usgrexmpl  26155  griedg0ssusgr  26157  uhgrspanop  26188  uhgrspan1  26195  upgrres  26198  umgrres  26199  usgrres  26200  upgrres1  26205  umgrres1  26206  usgrres1  26207  nbupgruvtxres  26308  usgrexi  26337  cusgrexi  26339  cffldtocusgr  26343  cusgrres  26344  vtxdgop  26366  umgr2v2e  26421  wlkp1lem2  26571  wlkpwwlkf1ouspgr  26765  wlkwwlksur  26783  wwlksnext  26788  eupth2eucrct  27077  eupthvdres  27095  konigsbergumgr  27112  konigsbergupgrOLD  27113  numclwlk1lem2fv  27226  ex-br  27288  cnnvg  27533  cnnvs  27535  cnnvnm  27536  h2hva  27831  h2hsm  27832  h2hnm  27833  hhssva  28114  hhsssm  28115  hhssnm  28116  hhshsslem1  28124  br8d  29422  xppreima2  29450  aciunf1lem  29462  ofpreima  29465  cnvoprab  29498  smatrcl  29862  smatlem  29863  fvproj  29899  fimaproj  29900  txomap  29901  qtophaus  29903  hgt750lemb  30734  bnj97  30936  bnj553  30968  bnj966  31014  bnj1442  31117  erdszelem9  31181  erdszelem10  31182  txpconn  31214  txsconnlem  31222  msubval  31422  mvhval  31431  msubvrs  31457  brtpid1  31602  brtpid2  31603  brtpid3  31604  brtp  31639  dfpo2  31645  br8  31646  br6  31647  br4  31648  br1steq  31670  br2ndeq  31671  br1steqg  31672  br2ndeqg  31673  dfdm5  31676  dfrn5  31677  elima4  31679  fv1stcnv  31680  fv2ndcnv  31681  brtxp  31987  brpprod  31992  brpprod3b  31994  brsset  31996  brtxpsd  32001  dffun10  32021  elfuns  32022  brcart  32039  brimg  32044  brapply  32045  brcup  32046  brcap  32047  brsuccf  32048  brrestrict  32056  dfrecs2  32057  dfrdg4  32058  fvtransport  32139  brcolinear2  32165  colineardim1  32168  brsegle  32215  fvline  32251  ellines  32259  filnetlem3  32375  bj-inftyexpiinv  33095  bj-inftyexpidisj  33097  bj-elccinfty  33101  bj-minftyccb  33112  finxpreclem2  33227  finxp0  33228  finxp1o  33229  finxpreclem3  33230  finxpreclem4  33231  finxpreclem5  33232  finxpreclem6  33233  poimirlem9  33418  poimirlem15  33424  poimirlem17  33426  poimirlem20  33429  poimirlem24  33433  poimirlem28  33437  mblfinlem2  33447  heiborlem6  33615  heiborlem7  33616  heiborlem8  33617  grposnOLD  33681  rngosn3  33723  gidsn  33751  zrdivrng  33752  dvhvaddval  36379  dvhvscaval  36388  dibglbN  36455  dihglbcpreN  36589  dihmeetlem4preN  36595  dihmeetlem13N  36608  hdmapfval  37119  elcnvlem  37907  cotrintab  37921  elimaint  37940  snhesn  38080  projf1o  39386  dvnprodlem1  40161  dvnprodlem2  40162  sge0xp  40646  hoicvr  40762  hoicvrrex  40770  hoidmv1le  40808  hoi2toco  40821  ovnlecvr2  40824  ovolval5lem2  40867  setsidel  41346  opeliun2xp  42111  lmod1lem2  42277  lmod1lem3  42278  lmod1zr  42282  zlmodzxznm  42286  zlmodzxzldeplem  42287