Theorem opex 5439

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 4846	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5407	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5277	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4551	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2830	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2108  Vcvv 3459  ∅c0 4308  ifcif 4500  {csn 4601  {cpr 4603  ⟨cop 4607

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608

This theorem is referenced by:  otex  5440  brv  5447  otth2  5458  otthg  5460  sbcop1  5463  oteqex2  5474  oteqex  5475  snopeqop  5481  propeqop  5482  propssopi  5483  euop2  5487  brsnop  5497  brtp  5498  opabidw  5499  opabid  5500  elopab  5502  rexopabb  5503  opabn0  5528  opeliunxp  5721  opeliun2xp  5722  elvvv  5730  opbrop  5752  relsnopg  5782  xpiindi  5815  raliunxp  5819  idrefALT  6100  intirr  6107  xpnz  6148  dmsnn0  6196  dmsnopg  6202  cnvcnvsn  6208  op2ndb  6216  opswap  6218  cnviin  6275  reuop  6282  dfpo2  6285  funopg  6569  dffv2  6973  fsn  7124  f1o2sn  7131  idref  7135  funsndifnop  7140  fmptsng  7159  fmptsnd  7160  fvsng  7171  resfunexg  7206  fveqf1o  7294  fliftel  7301  fliftel1  7302  oprabidw  7434  oprabid  7435  dfoprab2  7463  oprabv  7465  rnoprab  7510  eloprabga  7514  ot1stg  8000  ot2ndg  8001  ot3rdg  8002  fo1st  8006  fo2nd  8007  br1steqg  8008  br2ndeqg  8009  opiota  8056  eloprabi  8060  mposn  8100  fpar  8113  fsplitfpar  8115  opco1  8120  opco2  8121  frxp  8123  xporderlem  8124  fnwelem  8128  fvproj  8131  fimaproj  8132  xpord2lem  8139  xpord2pred  8142  xpord2indlem  8144  frxp3  8148  mpoxopoveq  8216  brtpos  8232  dmtpos  8235  rntpos  8236  tpostpos  8243  wfrlem14OLD  8334  tfrlem11  8400  seqomlem1  8462  seqomlem3  8464  seqomlem4  8465  omeu  8595  naddcllem  8686  iiner  8801  xpsnen  9067  xpcomco  9074  xpassen  9078  xpmapenlem  9156  dif1en  9172  dif1enOLD  9174  unxpdomlem1  9256  inlresf  9926  inrresf  9928  djur  9931  djuss  9932  djuun  9938  1stinl  9939  2ndinl  9940  1stinr  9941  2ndinr  9942  fseqenlem2  10037  dju1dif  10185  fpwwe  10658  addpipq2  10948  addpqnq  10950  mulpipq2  10951  mulpqnq  10953  ordpipq  10954  prlem934  11045  addcnsr  11147  mulcnsr  11148  ltresr  11152  addcnsrec  11155  mulcnsrec  11156  axcnre  11176  om2uzrdg  13972  uzrdg0i  13975  uzrdgsuci  13976  hashfun  14453  wrdexb  14541  s1len  14622  s1nz  14623  s111  14631  wrdlen2i  14959  brintclab  15018  fsumcnv  15787  fprodcnv  15997  ruclem1  16247  ruclem4  16250  eucalgval2  16598  crth  16795  phimullem  16796  setsval  17184  setsdm  17187  setsfun  17188  setsfun0  17189  setsexstruct2  17192  setsres  17195  setscom  17197  strfv  17220  setsid  17224  imasaddfnlem  17540  imasaddvallem  17541  imasvscafn  17549  idfuval  17887  cofuval  17893  resfval  17903  resfval2  17904  elhoma  18043  embedsetcestrclem  18167  xpcco  18193  xpcid  18199  1stfval  18201  2ndfval  18204  prfval  18209  prf1  18210  prf2  18212  evlfval  18227  curfval  18233  curf1  18235  curfcl  18242  hofval  18262  intopsn  18630  mgm1  18634  sgrp1  18705  mnd1  18755  mnd1id  18756  grpss  18935  grp1  19028  symg2bas  19372  efgmval  19691  efgi  19698  efgi2  19704  frgpnabllem1  19852  frgpnabllem2  19853  ring1  20268  rngqiprngimfv  21257  rngqiprngimf1  21259  opsrtoslem2  22012  mat1dimelbas  22407  mat1dimbas  22408  mat1dimscm  22411  mat1dimmul  22412  mat1f1o  22414  mat1rhmelval  22416  mvmulfval  22478  m2detleib  22567  txcnp  23556  upxp  23559  uptx  23561  txdis1cn  23571  hauseqlcld  23582  txlm  23584  xkoinjcn  23623  txflf  23942  qustgplem  24057  ucnima  24217  ucnprima  24218  fmucndlem  24227  imasdsf1olem  24310  cnheiborlem  24902  ovollb2lem  25439  ovolctb  25441  ovolshftlem1  25460  ovolscalem1  25464  ovolicc1  25467  ioombl1lem3  25511  ioombl1lem4  25512  ioorval  25525  dyadval  25543  mbfimaopnlem  25606  limccnp2  25843  addsval  27912  mulsval  28052  precsexlem1  28148  precsexlem2  28149  precsexlem3  28150  om2noseqrdg  28227  noseqrdg0  28230  noseqrdgsuc  28231  brbtwn  28824  brcgr  28825  eengbas  28906  ebtwntg  28907  ecgrtg  28908  elntg  28909  structvtxval  28946  structgrssvtx  28949  structgrssiedg  28950  gropd  28956  isuhgrop  28995  uhgrunop  29000  upgrop  29019  upgr0eop  29039  upgrunop  29044  umgrunop  29046  isuspgrop  29086  isusgrop  29087  ausgrusgrb  29090  usgr0eop  29171  griedg0ssusgr  29190  uhgrspanop  29221  uhgrspan1  29228  upgrres  29231  umgrres  29232  usgrres  29233  upgrres1  29238  umgrres1  29239  usgrres1  29240  usgrexi  29366  cusgrexi  29368  cffldtocusgr  29372  cffldtocusgrOLD  29373  cusgrres  29374  vtxdgop  29396  umgr2v2e  29451  wlkp1lem2  29600  wlkswwlksf1o  29807  wwlksnext  29821  eupth2eucrct  30144  eupthvdres  30162  konigsbergumgr  30178  numclwwlk1lem2fv  30283  numclwlk1lem1  30296  ex-br  30358  ex-fpar  30389  cnnvg  30605  cnnvs  30607  cnnvnm  30608  h2hva  30901  h2hsm  30902  h2hnm  30903  hhssva  31184  hhsssm  31185  hhssnm  31186  hhshsslem1  31194  br8d  32536  xppreima2  32575  aciunf1lem  32586  ofpreima  32589  rlocaddval  33209  rlocmulval  33210  linds2eq  33342  smatrcl  33773  smatlem  33774  txomap  33811  qtophaus  33813  hgt750lemb  34634  bnj97  34843  bnj553  34875  bnj966  34921  bnj1442  35026  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  35684  brtpid2  35685  brtpid3  35686  br8  35719  br6  35720  br4  35721  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  36344  bj-inftyexpitaufo  37166  bj-inftyexpitaudisj  37169  bj-inftyexpiinv  37172  bj-inftyexpidisj  37174  bj-elccinfty  37178  bj-minftyccb  37189  finxpreclem2  37354  finxp0  37355  finxp1o  37356  finxpreclem3  37357  finxpreclem4  37358  finxpreclem5  37359  finxpreclem6  37360  poimirlem9  37599  poimirlem15  37605  poimirlem17  37607  poimirlem20  37610  poimirlem24  37614  poimirlem28  37618  mblfinlem2  37628  heiborlem6  37786  heiborlem7  37787  heiborlem8  37788  grposnOLD  37852  rngosn3  37894  gidsn  37922  zrdivrng  37923  brxrn  38338  br1cossxrnres  38412  dvhvaddval  41055  dvhvscaval  41064  dibglbN  41131  dihglbcpreN  41265  dihmeetlem4preN  41271  dihmeetlem13N  41284  hdmapfval  41792  elcnvlem  43572  cotrintab  43585  elimaint  43620  snhesn  43757  projf1o  45169  dvnprodlem1  45923  dvnprodlem2  45924  sge0xp  46406  hoicvr  46525  hoicvrrex  46533  hoidmv1le  46571  hoi2toco  46584  ovnlecvr2  46587  ovolval5lem2  46630  fsetsnf1  47029  setsidel  47338  prproropf1olem3  47467  prproropf1olem4  47468  prproropreud  47471  isisubgr  47823  ushggricedg  47888  gpgusgralem  48008  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg3nbgrvtx0  48026  gpg3nbgrvtx0ALT  48027  gpg3nbgrvtx1  48028  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  gpg3kgrtriex  48039  gpgprismgr4cycllem2  48043  gpgprismgr4cycllem6  48047  gpgprismgr4cycllem7  48048  gpgprismgr4cycllem10  48051  lmod1lem2  48412  lmod1lem3  48413  lmod1zr  48417  zlmodzxznm  48421  zlmodzxzldeplem  48422  rrx2xpref1o  48646  line2x  48682  inlinecirc02plem  48714  iinxp  48757  ovsng  48782  eloprab1st2nd  48791  tposid  48808  tposidres  48809  rescofuf  49004  idfurcl  49006  imaf1hom  49015  oppfvalg  49022  oppfrcl  49024  swapfval  49127  swapf1a  49134  swapf2a  49136  swapf1  49137  swapf2  49139  fucofvalg  49177  fucofval  49178  fucofvalne  49184  fuco21  49195  fucof21  49206  prcofvalg  49235  prcofvala  49236  prcofval  49237  thincciso  49287  setc1ocofval  49327  functermceu  49343  termcfuncval  49365  relran  49447  ranrcl4lem  49460  ranup  49464