Theorem opex 5404

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 4822	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5375	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5245	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4526	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2827	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2111  Vcvv 3436  ∅c0 4283  ifcif 4475  {csn 4576  {cpr 4578  ⟨cop 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583

This theorem is referenced by:  otex  5405  brv  5412  otth2  5423  otthg  5425  sbcop1  5428  oteqex2  5439  oteqex  5440  snopeqop  5446  propeqop  5447  propssopi  5448  euop2  5452  brsnop  5462  brtp  5463  opabidw  5464  opabid  5465  elopab  5467  rexopabb  5468  opabn0  5493  opeliunxp  5683  opeliun2xp  5684  elvvv  5692  opbrop  5714  relsnopg  5743  xpiindi  5775  raliunxp  5779  idrefALT  6060  intirr  6065  xpnz  6106  dmsnn0  6154  dmsnopg  6160  cnvcnvsn  6166  op2ndb  6174  opswap  6176  cnviin  6233  reuop  6240  dfpo2  6243  funopg  6515  dffv2  6917  fsn  7068  f1o2sn  7075  idref  7079  funsndifnop  7084  fmptsng  7102  fmptsnd  7103  fvsng  7114  resfunexg  7149  fveqf1o  7236  fliftel  7243  fliftel1  7244  oprabidw  7377  oprabid  7378  dfoprab2  7404  oprabv  7406  rnoprab  7451  eloprabga  7455  ot1stg  7935  ot2ndg  7936  ot3rdg  7937  fo1st  7941  fo2nd  7942  br1steqg  7943  br2ndeqg  7944  opiota  7991  eloprabi  7995  mposn  8033  fpar  8046  fsplitfpar  8048  opco1  8053  opco2  8054  frxp  8056  xporderlem  8057  fnwelem  8061  fvproj  8064  fimaproj  8065  xpord2lem  8072  xpord2pred  8075  xpord2indlem  8077  frxp3  8081  mpoxopoveq  8149  brtpos  8165  dmtpos  8168  rntpos  8169  tpostpos  8176  tfrlem11  8307  seqomlem1  8369  seqomlem3  8371  seqomlem4  8372  omeu  8500  naddcllem  8591  iiner  8713  xpsnen  8974  xpcomco  8980  xpassen  8984  xpmapenlem  9057  dif1en  9071  unxpdomlem1  9140  inlresf  9807  inrresf  9809  djur  9812  djuss  9813  djuun  9819  1stinl  9820  2ndinl  9821  1stinr  9822  2ndinr  9823  fseqenlem2  9916  dju1dif  10064  fpwwe  10537  addpipq2  10827  addpqnq  10829  mulpipq2  10830  mulpqnq  10832  ordpipq  10833  prlem934  10924  addcnsr  11026  mulcnsr  11027  ltresr  11031  addcnsrec  11034  mulcnsrec  11035  axcnre  11055  om2uzrdg  13863  uzrdg0i  13866  uzrdgsuci  13867  hashfun  14344  wrdexb  14432  s1len  14514  s1nz  14515  s111  14523  wrdlen2i  14849  brintclab  14908  fsumcnv  15680  fprodcnv  15890  ruclem1  16140  ruclem4  16143  eucalgval2  16492  crth  16689  phimullem  16690  setsval  17078  setsdm  17081  setsfun  17082  setsfun0  17083  setsexstruct2  17086  setsres  17089  setscom  17091  strfv  17114  setsid  17118  imasaddfnlem  17432  imasaddvallem  17433  imasvscafn  17441  idfuval  17783  cofuval  17789  resfval  17799  resfval2  17800  elhoma  17939  embedsetcestrclem  18063  xpcco  18089  xpcid  18095  1stfval  18097  2ndfval  18100  prfval  18105  prf1  18106  prf2  18108  evlfval  18123  curfval  18129  curf1  18131  curfcl  18138  hofval  18158  intopsn  18562  mgm1  18566  sgrp1  18637  mnd1  18687  mnd1id  18688  grpss  18867  grp1  18960  symg2bas  19306  efgmval  19625  efgi  19632  efgi2  19638  frgpnabllem1  19786  frgpnabllem2  19787  ring1  20229  rngqiprngimfv  21236  rngqiprngimf1  21238  opsrtoslem2  21992  mat1dimelbas  22387  mat1dimbas  22388  mat1dimscm  22391  mat1dimmul  22392  mat1f1o  22394  mat1rhmelval  22396  mvmulfval  22458  m2detleib  22547  txcnp  23536  upxp  23539  uptx  23541  txdis1cn  23551  hauseqlcld  23562  txlm  23564  xkoinjcn  23603  txflf  23922  qustgplem  24037  ucnima  24196  ucnprima  24197  fmucndlem  24206  imasdsf1olem  24289  cnheiborlem  24881  ovollb2lem  25417  ovolctb  25419  ovolshftlem1  25438  ovolscalem1  25442  ovolicc1  25445  ioombl1lem3  25489  ioombl1lem4  25490  ioorval  25503  dyadval  25521  mbfimaopnlem  25584  limccnp2  25821  addsval  27906  mulsval  28049  precsexlem1  28146  precsexlem2  28147  precsexlem3  28148  om2noseqrdg  28235  noseqrdg0  28238  noseqrdgsuc  28239  brbtwn  28878  brcgr  28879  eengbas  28960  ebtwntg  28961  ecgrtg  28962  elntg  28963  structvtxval  29000  structgrssvtx  29003  structgrssiedg  29004  gropd  29010  isuhgrop  29049  uhgrunop  29054  upgrop  29073  upgr0eop  29093  upgrunop  29098  umgrunop  29100  isuspgrop  29140  isusgrop  29141  ausgrusgrb  29144  usgr0eop  29225  griedg0ssusgr  29244  uhgrspanop  29275  uhgrspan1  29282  upgrres  29285  umgrres  29286  usgrres  29287  upgrres1  29292  umgrres1  29293  usgrres1  29294  usgrexi  29420  cusgrexi  29422  cffldtocusgr  29426  cffldtocusgrOLD  29427  cusgrres  29428  vtxdgop  29450  umgr2v2e  29505  wlkp1lem2  29652  wlkswwlksf1o  29858  wwlksnext  29872  eupth2eucrct  30195  eupthvdres  30213  konigsbergumgr  30229  numclwwlk1lem2fv  30334  numclwlk1lem1  30347  ex-br  30409  ex-fpar  30440  cnnvg  30656  cnnvs  30658  cnnvnm  30659  h2hva  30952  h2hsm  30953  h2hnm  30954  hhssva  31235  hhsssm  31236  hhssnm  31237  hhshsslem1  31245  br8d  32589  xppreima2  32631  aciunf1lem  32642  ofpreima  32645  rlocaddval  33233  rlocmulval  33234  linds2eq  33344  smatrcl  33807  smatlem  33808  txomap  33845  qtophaus  33847  hgt750lemb  34667  bnj97  34876  bnj553  34908  bnj966  34954  bnj1442  35059  erdszelem9  35241  erdszelem10  35242  txpconn  35274  txsconnlem  35282  goel  35389  goeleq12bg  35391  gonafv  35392  gonanegoal  35394  sat1el2xp  35421  fmlaomn0  35432  gonan0  35434  goaln0  35435  gonarlem  35436  gonar  35437  goalrlem  35438  goalr  35439  fmla0disjsuc  35440  fmlasucdisj  35441  satffunlem  35443  satffunlem1lem1  35444  satffunlem2lem1  35446  satfv0fvfmla0  35455  sategoelfvb  35461  prv1n  35473  msubval  35567  mvhval  35576  msubvrs  35602  brtpid1  35763  brtpid2  35764  brtpid3  35765  br8  35798  br6  35799  br4  35800  dfdm5  35815  dfrn5  35816  elima4  35818  fv1stcnv  35819  fv2ndcnv  35820  brtxp  35920  brpprod  35925  brpprod3b  35927  brsset  35929  brtxpsd  35934  dffun10  35954  elfuns  35955  brcart  35972  brimg  35977  brapply  35978  brcup  35979  brcap  35980  brsuccf  35981  brrestrict  35989  dfrecs2  35990  dfrdg4  35991  fvtransport  36072  brcolinear2  36098  colineardim1  36101  brsegle  36148  fvline  36184  ellines  36192  filnetlem3  36420  bj-inftyexpitaufo  37242  bj-inftyexpitaudisj  37245  bj-inftyexpiinv  37248  bj-inftyexpidisj  37250  bj-elccinfty  37254  bj-minftyccb  37265  finxpreclem2  37430  finxp0  37431  finxp1o  37432  finxpreclem3  37433  finxpreclem4  37434  finxpreclem5  37435  finxpreclem6  37436  poimirlem9  37675  poimirlem15  37681  poimirlem17  37683  poimirlem20  37686  poimirlem24  37690  poimirlem28  37694  mblfinlem2  37704  heiborlem6  37862  heiborlem7  37863  heiborlem8  37864  grposnOLD  37928  rngosn3  37970  gidsn  37998  zrdivrng  37999  brxrn  38408  br1cossxrnres  38491  dvhvaddval  41135  dvhvscaval  41144  dibglbN  41211  dihglbcpreN  41345  dihmeetlem4preN  41351  dihmeetlem13N  41364  hdmapfval  41872  elcnvlem  43640  cotrintab  43653  elimaint  43688  snhesn  43825  nregmodellem  45055  projf1o  45240  dvnprodlem1  45990  dvnprodlem2  45991  sge0xp  46473  hoicvr  46592  hoicvrrex  46600  hoidmv1le  46638  hoi2toco  46651  ovnlecvr2  46654  ovolval5lem2  46697  fsetsnf1  47089  setsidel  47413  prproropf1olem3  47542  prproropf1olem4  47543  prproropreud  47546  isisubgr  47899  ushggricedg  47964  gpgusgralem  48093  gpgvtxedg0  48100  gpgvtxedg1  48101  gpg5nbgrvtx03starlem1  48105  gpg5nbgrvtx03starlem2  48106  gpg5nbgrvtx03starlem3  48107  gpg5nbgrvtx13starlem1  48108  gpg5nbgrvtx13starlem2  48109  gpg5nbgrvtx13starlem3  48110  gpg3nbgrvtx0  48113  gpg3nbgrvtx0ALT  48114  gpg3nbgrvtx1  48115  gpg5nbgrvtx03star  48117  gpg5nbgr3star  48118  gpg3kgrtriex  48126  gpgprismgr4cycllem2  48133  gpgprismgr4cycllem6  48137  gpgprismgr4cycllem7  48138  gpgprismgr4cycllem10  48141  gpg5edgnedg  48167  lmod1lem2  48526  lmod1lem3  48527  lmod1zr  48531  zlmodzxznm  48535  zlmodzxzldeplem  48536  rrx2xpref1o  48756  line2x  48792  inlinecirc02plem  48824  iinxp  48868  ovsng  48895  eloprab1st2nd  48905  tposid  48922  tposidres  48923  initc  49129  rescofuf  49131  idfurcl  49136  imaf1hom  49146  oppffn  49162  oppfvalg  49164  swapfval  49300  swapf1a  49307  swapf2a  49309  swapf1  49310  swapf2  49312  fucofvalg  49356  fucofval  49357  fucofvalne  49363  fuco21  49374  fucof21  49385  prcofvalg  49414  prcofvala  49415  prcofval  49416  thincciso  49491  setc1ocofval  49532  functermceu  49548  termcfuncval  49570  fucterm  49580  0fucterm  49581  relran  49662  ranval3  49669  ranrcl4lem  49676  ranup  49680  initocmd  49707