Theorem opex 5469

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 4870	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5437	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5307	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4576	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2837	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2108  Vcvv 3480  ∅c0 4333  ifcif 4525  {csn 4626  {cpr 4628  ⟨cop 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633

This theorem is referenced by:  otex  5470  brv  5477  otth2  5488  otthg  5490  sbcop1  5493  oteqex2  5504  oteqex  5505  snopeqop  5511  propeqop  5512  propssopi  5513  euop2  5517  brsnop  5527  brtp  5528  opabidw  5529  opabid  5530  elopab  5532  rexopabb  5533  opabn0  5558  opeliunxp  5752  opeliun2xp  5753  elvvv  5761  opbrop  5783  relsnopg  5813  xpiindi  5846  raliunxp  5850  idrefALT  6131  intirr  6138  xpnz  6179  dmsnn0  6227  dmsnopg  6233  cnvcnvsn  6239  op2ndb  6247  opswap  6249  cnviin  6306  reuop  6313  dfpo2  6316  funopg  6600  dffv2  7004  fsn  7155  f1o2sn  7162  idref  7166  funsndifnop  7171  fmptsng  7188  fmptsnd  7189  fvsng  7200  resfunexg  7235  fveqf1o  7322  fliftel  7329  fliftel1  7330  oprabidw  7462  oprabid  7463  dfoprab2  7491  oprabv  7493  rnoprab  7538  eloprabga  7542  ot1stg  8028  ot2ndg  8029  ot3rdg  8030  fo1st  8034  fo2nd  8035  br1steqg  8036  br2ndeqg  8037  opiota  8084  eloprabi  8088  mposn  8128  fpar  8141  fsplitfpar  8143  opco1  8148  opco2  8149  frxp  8151  xporderlem  8152  fnwelem  8156  fvproj  8159  fimaproj  8160  xpord2lem  8167  xpord2pred  8170  xpord2indlem  8172  frxp3  8176  mpoxopoveq  8244  brtpos  8260  dmtpos  8263  rntpos  8264  tpostpos  8271  wfrlem14OLD  8362  tfrlem11  8428  seqomlem1  8490  seqomlem3  8492  seqomlem4  8493  omeu  8623  naddcllem  8714  iiner  8829  xpsnen  9095  xpcomco  9102  xpassen  9106  xpmapenlem  9184  dif1en  9200  dif1enOLD  9202  unxpdomlem1  9286  inlresf  9954  inrresf  9956  djur  9959  djuss  9960  djuun  9966  1stinl  9967  2ndinl  9968  1stinr  9969  2ndinr  9970  fseqenlem2  10065  dju1dif  10213  fpwwe  10686  addpipq2  10976  addpqnq  10978  mulpipq2  10979  mulpqnq  10981  ordpipq  10982  prlem934  11073  addcnsr  11175  mulcnsr  11176  ltresr  11180  addcnsrec  11183  mulcnsrec  11184  axcnre  11204  om2uzrdg  13997  uzrdg0i  14000  uzrdgsuci  14001  hashfun  14476  wrdexb  14563  s1len  14644  s1nz  14645  s111  14653  wrdlen2i  14981  brintclab  15040  fsumcnv  15809  fprodcnv  16019  ruclem1  16267  ruclem4  16270  eucalgval2  16618  crth  16815  phimullem  16816  setsval  17204  setsdm  17207  setsfun  17208  setsfun0  17209  setsexstruct2  17212  setsres  17215  setscom  17217  strfv  17240  setsid  17244  imasaddfnlem  17573  imasaddvallem  17574  imasvscafn  17582  idfuval  17921  cofuval  17927  resfval  17937  resfval2  17938  elhoma  18077  embedsetcestrclem  18202  xpcco  18228  xpcid  18234  1stfval  18236  2ndfval  18239  prfval  18244  prf1  18245  prf2  18247  evlfval  18262  curfval  18268  curf1  18270  curfcl  18277  hofval  18297  intopsn  18667  mgm1  18671  sgrp1  18742  mnd1  18792  mnd1id  18793  grpss  18972  grp1  19065  symg2bas  19410  efgmval  19730  efgi  19737  efgi2  19743  frgpnabllem1  19891  frgpnabllem2  19892  ring1  20307  rngqiprngimfv  21308  rngqiprngimf1  21310  opsrtoslem2  22080  mat1dimelbas  22477  mat1dimbas  22478  mat1dimscm  22481  mat1dimmul  22482  mat1f1o  22484  mat1rhmelval  22486  mvmulfval  22548  m2detleib  22637  txcnp  23628  upxp  23631  uptx  23633  txdis1cn  23643  hauseqlcld  23654  txlm  23656  xkoinjcn  23695  txflf  24014  qustgplem  24129  ucnima  24290  ucnprima  24291  fmucndlem  24300  imasdsf1olem  24383  cnheiborlem  24986  ovollb2lem  25523  ovolctb  25525  ovolshftlem1  25544  ovolscalem1  25548  ovolicc1  25551  ioombl1lem3  25595  ioombl1lem4  25596  ioorval  25609  dyadval  25627  mbfimaopnlem  25690  limccnp2  25927  addsval  27995  mulsval  28135  precsexlem1  28231  precsexlem2  28232  precsexlem3  28233  om2noseqrdg  28310  noseqrdg0  28313  noseqrdgsuc  28314  brbtwn  28914  brcgr  28915  eengbas  28996  ebtwntg  28997  ecgrtg  28998  elntg  28999  structvtxval  29038  structgrssvtx  29041  structgrssiedg  29042  gropd  29048  isuhgrop  29087  uhgrunop  29092  upgrop  29111  upgr0eop  29131  upgrunop  29136  umgrunop  29138  isuspgrop  29178  isusgrop  29179  ausgrusgrb  29182  usgr0eop  29263  griedg0ssusgr  29282  uhgrspanop  29313  uhgrspan1  29320  upgrres  29323  umgrres  29324  usgrres  29325  upgrres1  29330  umgrres1  29331  usgrres1  29332  usgrexi  29458  cusgrexi  29460  cffldtocusgr  29464  cffldtocusgrOLD  29465  cusgrres  29466  vtxdgop  29488  umgr2v2e  29543  wlkp1lem2  29692  wlkswwlksf1o  29899  wwlksnext  29913  eupth2eucrct  30236  eupthvdres  30254  konigsbergumgr  30270  numclwwlk1lem2fv  30375  numclwlk1lem1  30388  ex-br  30450  ex-fpar  30481  cnnvg  30697  cnnvs  30699  cnnvnm  30700  h2hva  30993  h2hsm  30994  h2hnm  30995  hhssva  31276  hhsssm  31277  hhssnm  31278  hhshsslem1  31286  br8d  32622  xppreima2  32661  aciunf1lem  32672  ofpreima  32675  rlocaddval  33272  rlocmulval  33273  linds2eq  33409  smatrcl  33795  smatlem  33796  txomap  33833  qtophaus  33835  hgt750lemb  34671  bnj97  34880  bnj553  34912  bnj966  34958  bnj1442  35063  erdszelem9  35204  erdszelem10  35205  txpconn  35237  txsconnlem  35245  goel  35352  goeleq12bg  35354  gonafv  35355  gonanegoal  35357  sat1el2xp  35384  fmlaomn0  35395  gonan0  35397  goaln0  35398  gonarlem  35399  gonar  35400  goalrlem  35401  goalr  35402  fmla0disjsuc  35403  fmlasucdisj  35404  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  satfv0fvfmla0  35418  sategoelfvb  35424  prv1n  35436  msubval  35530  mvhval  35539  msubvrs  35565  brtpid1  35721  brtpid2  35722  brtpid3  35723  br8  35756  br6  35757  br4  35758  dfdm5  35773  dfrn5  35774  elima4  35776  fv1stcnv  35777  fv2ndcnv  35778  brtxp  35881  brpprod  35886  brpprod3b  35888  brsset  35890  brtxpsd  35895  dffun10  35915  elfuns  35916  brcart  35933  brimg  35938  brapply  35939  brcup  35940  brcap  35941  brsuccf  35942  brrestrict  35950  dfrecs2  35951  dfrdg4  35952  fvtransport  36033  brcolinear2  36059  colineardim1  36062  brsegle  36109  fvline  36145  ellines  36153  filnetlem3  36381  bj-inftyexpitaufo  37203  bj-inftyexpitaudisj  37206  bj-inftyexpiinv  37209  bj-inftyexpidisj  37211  bj-elccinfty  37215  bj-minftyccb  37226  finxpreclem2  37391  finxp0  37392  finxp1o  37393  finxpreclem3  37394  finxpreclem4  37395  finxpreclem5  37396  finxpreclem6  37397  poimirlem9  37636  poimirlem15  37642  poimirlem17  37644  poimirlem20  37647  poimirlem24  37651  poimirlem28  37655  mblfinlem2  37665  heiborlem6  37823  heiborlem7  37824  heiborlem8  37825  grposnOLD  37889  rngosn3  37931  gidsn  37959  zrdivrng  37960  brxrn  38375  br1cossxrnres  38449  dvhvaddval  41092  dvhvscaval  41101  dibglbN  41168  dihglbcpreN  41302  dihmeetlem4preN  41308  dihmeetlem13N  41321  hdmapfval  41829  elcnvlem  43614  cotrintab  43627  elimaint  43662  snhesn  43799  projf1o  45202  dvnprodlem1  45961  dvnprodlem2  45962  sge0xp  46444  hoicvr  46563  hoicvrrex  46571  hoidmv1le  46609  hoi2toco  46622  ovnlecvr2  46625  ovolval5lem2  46668  fsetsnf1  47064  setsidel  47363  prproropf1olem3  47492  prproropf1olem4  47493  prproropreud  47496  isisubgr  47848  ushggricedg  47896  gpgusgralem  48011  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg3nbgrvtx1  48034  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  gpg3kgrtriex  48045  lmod1lem2  48405  lmod1lem3  48406  lmod1zr  48410  zlmodzxznm  48414  zlmodzxzldeplem  48415  rrx2xpref1o  48639  line2x  48675  inlinecirc02plem  48707  tposid  48785  tposidres  48786  rescofuf  48922  swapfval  48968  swapf1a  48975  swapf2a  48977  swapf1  48978  swapf2  48980  fucofvalg  49013  fucofval  49014  fucofvalne  49020  fuco21  49031  fucof21  49042  thincciso  49102  functermceu  49142  mndtchom  49181