Theorem opex 5470

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 4876	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5438	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5312	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4583	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2822	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 394   ∈ wcel 2099  Vcvv 3462  ∅c0 4325  ifcif 4533  {csn 4633  {cpr 4635  ⟨cop 4639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640

This theorem is referenced by:  otex  5471  brv  5478  otth2  5489  otthg  5491  sbcop1  5494  oteqex2  5505  oteqex  5506  snopeqop  5512  propeqop  5513  propssopi  5514  euop2  5518  brsnop  5528  brtp  5529  opabidw  5530  opabid  5531  elopab  5533  rexopabb  5534  opabn0  5559  opeliunxp  5749  elvvv  5757  opbrop  5779  relsnopg  5809  xpiindi  5842  raliunxp  5846  idrefALT  6123  intirr  6130  xpnz  6170  dmsnn0  6218  dmsnopg  6224  cnvcnvsn  6230  op2ndb  6238  opswap  6240  cnviin  6297  reuop  6304  dfpo2  6307  funopg  6593  dffv2  6997  fsn  7149  f1o2sn  7156  idref  7160  funsndifnop  7165  fmptsng  7182  fmptsnd  7183  fvsng  7194  resfunexg  7232  fveqf1o  7316  fliftel  7321  fliftel1  7322  oprabidw  7455  oprabid  7456  dfoprab2  7483  oprabv  7485  rnoprab  7529  eloprabga  7533  eloprabgaOLD  7534  ot1stg  8017  ot2ndg  8018  ot3rdg  8019  fo1st  8023  fo2nd  8024  br1steqg  8025  br2ndeqg  8026  opiota  8073  eloprabi  8077  mposn  8117  fpar  8130  fsplitfpar  8132  opco1  8137  opco2  8138  frxp  8140  xporderlem  8141  fnwelem  8145  fvproj  8148  fimaproj  8149  xpord2lem  8156  xpord2pred  8159  xpord2indlem  8161  frxp3  8165  mpoxopoveq  8234  brtpos  8250  dmtpos  8253  rntpos  8254  tpostpos  8261  wfrlem14OLD  8352  tfrlem11  8418  seqomlem1  8480  seqomlem3  8482  seqomlem4  8483  omeu  8615  naddcllem  8706  iiner  8818  xpsnen  9093  xpcomco  9100  xpassen  9104  xpmapenlem  9182  dif1en  9198  dif1enOLD  9200  unxpdomlem1  9284  inlresf  9957  inrresf  9959  djur  9962  djuss  9963  djuun  9969  1stinl  9970  2ndinl  9971  1stinr  9972  2ndinr  9973  fseqenlem2  10068  dju1dif  10215  fpwwe  10689  addpipq2  10979  addpqnq  10981  mulpipq2  10982  mulpqnq  10984  ordpipq  10985  prlem934  11076  addcnsr  11178  mulcnsr  11179  ltresr  11183  addcnsrec  11186  mulcnsrec  11187  axcnre  11207  om2uzrdg  13976  uzrdg0i  13979  uzrdgsuci  13980  hashfun  14454  wrdexb  14533  s1len  14614  s1nz  14615  s111  14623  wrdlen2i  14951  brintclab  15006  fsumcnv  15777  fprodcnv  15985  ruclem1  16233  ruclem4  16236  eucalgval2  16582  crth  16780  phimullem  16781  setsval  17169  setsdm  17172  setsfun  17173  setsfun0  17174  setsexstruct2  17177  setsres  17180  setscom  17182  strfv  17206  setsid  17210  imasaddfnlem  17543  imasaddvallem  17544  imasvscafn  17552  idfuval  17895  cofuval  17901  resfval  17911  resfval2  17912  elhoma  18054  embedsetcestrclem  18181  xpcco  18207  xpcid  18213  1stfval  18215  2ndfval  18218  prfval  18223  prf1  18224  prf2  18226  evlfval  18242  curfval  18248  curf1  18250  curfcl  18257  hofval  18277  intopsn  18647  mgm1  18651  sgrp1  18722  mnd1  18769  mnd1id  18770  grpss  18949  grp1  19041  symg2bas  19390  efgmval  19710  efgi  19717  efgi2  19723  frgpnabllem1  19871  frgpnabllem2  19872  ring1  20289  rngqiprngimfv  21287  rngqiprngimf1  21289  opsrtoslem2  22069  mat1dimelbas  22464  mat1dimbas  22465  mat1dimscm  22468  mat1dimmul  22469  mat1f1o  22471  mat1rhmelval  22473  mvmulfval  22535  m2detleib  22624  txcnp  23615  upxp  23618  uptx  23620  txdis1cn  23630  hauseqlcld  23641  txlm  23643  xkoinjcn  23682  txflf  24001  qustgplem  24116  ucnima  24277  ucnprima  24278  fmucndlem  24287  imasdsf1olem  24370  cnheiborlem  24971  ovollb2lem  25508  ovolctb  25510  ovolshftlem1  25529  ovolscalem1  25533  ovolicc1  25536  ioombl1lem3  25580  ioombl1lem4  25581  ioorval  25594  dyadval  25612  mbfimaopnlem  25675  limccnp2  25912  addsval  27976  mulsval  28110  precsexlem1  28206  precsexlem2  28207  precsexlem3  28208  om2noseqrdg  28278  noseqrdg0  28281  noseqrdgsuc  28282  brbtwn  28833  brcgr  28834  eengbas  28915  ebtwntg  28916  ecgrtg  28917  elntg  28918  structvtxval  28957  structgrssvtx  28960  structgrssiedg  28961  gropd  28967  isuhgrop  29006  uhgrunop  29011  upgrop  29030  upgr0eop  29050  upgrunop  29055  umgrunop  29057  isuspgrop  29097  isusgrop  29098  ausgrusgrb  29101  usgr0eop  29182  usgrexmpl  29199  griedg0ssusgr  29201  uhgrspanop  29232  uhgrspan1  29239  upgrres  29242  umgrres  29243  usgrres  29244  upgrres1  29249  umgrres1  29250  usgrres1  29251  usgrexi  29377  cusgrexi  29379  cffldtocusgr  29383  cffldtocusgrOLD  29384  cusgrres  29385  vtxdgop  29407  umgr2v2e  29462  wlkp1lem2  29611  wlkswwlksf1o  29813  wwlksnext  29827  eupth2eucrct  30150  eupthvdres  30168  konigsbergumgr  30184  numclwwlk1lem2fv  30289  numclwlk1lem1  30302  ex-br  30364  ex-fpar  30395  cnnvg  30611  cnnvs  30613  cnnvnm  30614  h2hva  30907  h2hsm  30908  h2hnm  30909  hhssva  31190  hhsssm  31191  hhssnm  31192  hhshsslem1  31200  br8d  32530  xppreima2  32568  aciunf1lem  32579  ofpreima  32582  cnvoprabOLD  32634  rlocaddval  33123  rlocmulval  33124  linds2eq  33256  smatrcl  33611  smatlem  33612  txomap  33649  qtophaus  33651  hgt750lemb  34502  bnj97  34711  bnj553  34743  bnj966  34789  bnj1442  34894  erdszelem9  35027  erdszelem10  35028  txpconn  35060  txsconnlem  35068  goel  35175  goeleq12bg  35177  gonafv  35178  gonanegoal  35180  sat1el2xp  35207  fmlaomn0  35218  gonan0  35220  goaln0  35221  gonarlem  35222  gonar  35223  goalrlem  35224  goalr  35225  fmla0disjsuc  35226  fmlasucdisj  35227  satffunlem  35229  satffunlem1lem1  35230  satffunlem2lem1  35232  satfv0fvfmla0  35241  sategoelfvb  35247  prv1n  35259  msubval  35353  mvhval  35362  msubvrs  35388  brtpid1  35543  brtpid2  35544  brtpid3  35545  br8  35578  br6  35579  br4  35580  dfdm5  35596  dfrn5  35597  elima4  35599  fv1stcnv  35600  fv2ndcnv  35601  brtxp  35704  brpprod  35709  brpprod3b  35711  brsset  35713  brtxpsd  35718  dffun10  35738  elfuns  35739  brcart  35756  brimg  35761  brapply  35762  brcup  35763  brcap  35764  brsuccf  35765  brrestrict  35773  dfrecs2  35774  dfrdg4  35775  fvtransport  35856  brcolinear2  35882  colineardim1  35885  brsegle  35932  fvline  35968  ellines  35976  filnetlem3  36092  bj-inftyexpitaufo  36909  bj-inftyexpitaudisj  36912  bj-inftyexpiinv  36915  bj-inftyexpidisj  36917  bj-elccinfty  36921  bj-minftyccb  36932  finxpreclem2  37097  finxp0  37098  finxp1o  37099  finxpreclem3  37100  finxpreclem4  37101  finxpreclem5  37102  finxpreclem6  37103  poimirlem9  37330  poimirlem15  37336  poimirlem17  37338  poimirlem20  37341  poimirlem24  37345  poimirlem28  37349  mblfinlem2  37359  heiborlem6  37517  heiborlem7  37518  heiborlem8  37519  grposnOLD  37583  rngosn3  37625  gidsn  37653  zrdivrng  37654  brxrn  38072  br1cossxrnres  38146  dvhvaddval  40789  dvhvscaval  40798  dibglbN  40865  dihglbcpreN  40999  dihmeetlem4preN  41005  dihmeetlem13N  41018  hdmapfval  41526  elcnvlem  43268  cotrintab  43281  elimaint  43316  snhesn  43453  projf1o  44804  dvnprodlem1  45567  dvnprodlem2  45568  sge0xp  46050  hoicvr  46169  hoicvrrex  46177  hoidmv1le  46215  hoi2toco  46228  ovnlecvr2  46231  ovolval5lem2  46274  fsetsnf1  46667  setsidel  46948  prproropf1olem3  47077  prproropf1olem4  47078  prproropreud  47081  isisubgr  47429  ushggricedg  47475  opeliun2xp  47711  lmod1lem2  47871  lmod1lem3  47872  lmod1zr  47876  zlmodzxznm  47880  zlmodzxzldeplem  47881  rrx2xpref1o  48106  line2x  48142  inlinecirc02plem  48174  thincciso  48370  mndtchom  48411