Theorem opex 5412

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 4826	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5382	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5252	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4530	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2832	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  ifcif 4479  {csn 4580  {cpr 4582  ⟨cop 4586

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  otex  5413  brv  5420  otth2  5431  otthg  5433  sbcop1  5436  oteqex2  5447  oteqex  5448  snopeqop  5454  propeqop  5455  propssopi  5456  euop2  5460  brsnop  5470  brtp  5471  opabidw  5472  opabid  5473  elopab  5475  rexopabb  5476  opabn0  5501  opeliunxp  5691  opeliun2xp  5692  elvvv  5700  opbrop  5722  relsnopg  5752  xpiindi  5784  raliunxp  5788  idrefALT  6070  intirr  6075  xpnz  6117  dmsnn0  6165  dmsnopg  6171  cnvcnvsn  6177  op2ndb  6185  opswap  6187  cnviin  6244  reuop  6251  dfpo2  6254  funopg  6526  dffv2  6929  fsn  7080  f1o2sn  7087  idref  7091  funsndifnop  7096  fmptsng  7114  fmptsnd  7115  fvsng  7126  resfunexg  7161  fveqf1o  7248  fliftel  7255  fliftel1  7256  oprabidw  7389  oprabid  7390  dfoprab2  7416  oprabv  7418  rnoprab  7463  eloprabga  7467  ot1stg  7947  ot2ndg  7948  ot3rdg  7949  fo1st  7953  fo2nd  7954  br1steqg  7955  br2ndeqg  7956  opiota  8003  eloprabi  8007  mposn  8045  fpar  8058  fsplitfpar  8060  opco1  8065  opco2  8066  frxp  8068  xporderlem  8069  fnwelem  8073  fvproj  8076  fimaproj  8077  xpord2lem  8084  xpord2pred  8087  xpord2indlem  8089  frxp3  8093  mpoxopoveq  8161  brtpos  8177  dmtpos  8180  rntpos  8181  tpostpos  8188  tfrlem11  8319  seqomlem1  8381  seqomlem3  8383  seqomlem4  8384  omeu  8512  naddcllem  8604  iiner  8726  xpsnen  8989  xpcomco  8995  xpassen  8999  xpmapenlem  9072  dif1en  9086  unxpdomlem1  9156  inlresf  9826  inrresf  9828  djur  9831  djuss  9832  djuun  9838  1stinl  9839  2ndinl  9840  1stinr  9841  2ndinr  9842  fseqenlem2  9935  dju1dif  10083  fpwwe  10557  addpipq2  10847  addpqnq  10849  mulpipq2  10850  mulpqnq  10852  ordpipq  10853  prlem934  10944  addcnsr  11046  mulcnsr  11047  ltresr  11051  addcnsrec  11054  mulcnsrec  11055  axcnre  11075  om2uzrdg  13879  uzrdg0i  13882  uzrdgsuci  13883  hashfun  14360  wrdexb  14448  s1len  14530  s1nz  14531  s111  14539  wrdlen2i  14865  brintclab  14924  fsumcnv  15696  fprodcnv  15906  ruclem1  16156  ruclem4  16159  eucalgval2  16508  crth  16705  phimullem  16706  setsval  17094  setsdm  17097  setsfun  17098  setsfun0  17099  setsexstruct2  17102  setsres  17105  setscom  17107  strfv  17130  setsid  17134  imasaddfnlem  17449  imasaddvallem  17450  imasvscafn  17458  idfuval  17800  cofuval  17806  resfval  17816  resfval2  17817  elhoma  17956  embedsetcestrclem  18080  xpcco  18106  xpcid  18112  1stfval  18114  2ndfval  18117  prfval  18122  prf1  18123  prf2  18125  evlfval  18140  curfval  18146  curf1  18148  curfcl  18155  hofval  18175  intopsn  18579  mgm1  18583  sgrp1  18654  mnd1  18704  mnd1id  18705  grpss  18884  grp1  18977  symg2bas  19322  efgmval  19641  efgi  19648  efgi2  19654  frgpnabllem1  19802  frgpnabllem2  19803  ring1  20245  rngqiprngimfv  21253  rngqiprngimf1  21255  opsrtoslem2  22011  mat1dimelbas  22415  mat1dimbas  22416  mat1dimscm  22419  mat1dimmul  22420  mat1f1o  22422  mat1rhmelval  22424  mvmulfval  22486  m2detleib  22575  txcnp  23564  upxp  23567  uptx  23569  txdis1cn  23579  hauseqlcld  23590  txlm  23592  xkoinjcn  23631  txflf  23950  qustgplem  24065  ucnima  24224  ucnprima  24225  fmucndlem  24234  imasdsf1olem  24317  cnheiborlem  24909  ovollb2lem  25445  ovolctb  25447  ovolshftlem1  25466  ovolscalem1  25470  ovolicc1  25473  ioombl1lem3  25517  ioombl1lem4  25518  ioorval  25531  dyadval  25549  mbfimaopnlem  25612  limccnp2  25849  addsval  27958  mulsval  28105  precsexlem1  28203  precsexlem2  28204  precsexlem3  28205  om2noseqrdg  28300  noseqrdg0  28303  noseqrdgsuc  28304  brbtwn  28972  brcgr  28973  eengbas  29054  ebtwntg  29055  ecgrtg  29056  elntg  29057  structvtxval  29094  structgrssvtx  29097  structgrssiedg  29098  gropd  29104  isuhgrop  29143  uhgrunop  29148  upgrop  29167  upgr0eop  29187  upgrunop  29192  umgrunop  29194  isuspgrop  29234  isusgrop  29235  ausgrusgrb  29238  usgr0eop  29319  griedg0ssusgr  29338  uhgrspanop  29369  uhgrspan1  29376  upgrres  29379  umgrres  29380  usgrres  29381  upgrres1  29386  umgrres1  29387  usgrres1  29388  usgrexi  29514  cusgrexi  29516  cffldtocusgr  29520  cffldtocusgrOLD  29521  cusgrres  29522  vtxdgop  29544  umgr2v2e  29599  wlkp1lem2  29746  wlkswwlksf1o  29952  wwlksnext  29966  eupth2eucrct  30292  eupthvdres  30310  konigsbergumgr  30326  numclwwlk1lem2fv  30431  numclwlk1lem1  30444  ex-br  30506  ex-fpar  30537  cnnvg  30753  cnnvs  30755  cnnvnm  30756  h2hva  31049  h2hsm  31050  h2hnm  31051  hhssva  31332  hhsssm  31333  hhssnm  31334  hhshsslem1  31342  br8d  32686  xppreima2  32729  aciunf1lem  32740  ofpreima  32743  rlocaddval  33350  rlocmulval  33351  linds2eq  33462  smatrcl  33953  smatlem  33954  txomap  33991  qtophaus  33993  hgt750lemb  34813  bnj97  35022  bnj553  35054  bnj966  35100  bnj1442  35205  erdszelem9  35393  erdszelem10  35394  txpconn  35426  txsconnlem  35434  goel  35541  goeleq12bg  35543  gonafv  35544  gonanegoal  35546  sat1el2xp  35573  fmlaomn0  35584  gonan0  35586  goaln0  35587  gonarlem  35588  gonar  35589  goalrlem  35590  goalr  35591  fmla0disjsuc  35592  fmlasucdisj  35593  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  satfv0fvfmla0  35607  sategoelfvb  35613  prv1n  35625  msubval  35719  mvhval  35728  msubvrs  35754  brtpid1  35915  brtpid2  35916  brtpid3  35917  br8  35950  br6  35951  br4  35952  dfdm5  35967  dfrn5  35968  elima4  35970  fv1stcnv  35971  fv2ndcnv  35972  brtxp  36072  brpprod  36077  brpprod3b  36079  brsset  36081  brtxpsd  36086  dffun10  36106  elfuns  36107  brcart  36124  brimg  36129  brapply  36130  brcup  36131  brcap  36132  lemsuccf  36133  brrestrict  36143  dfrecs2  36144  dfrdg4  36145  fvtransport  36226  brcolinear2  36252  colineardim1  36255  brsegle  36302  fvline  36338  ellines  36346  filnetlem3  36574  bj-inftyexpitaufo  37407  bj-inftyexpitaudisj  37410  bj-inftyexpiinv  37413  bj-inftyexpidisj  37415  bj-elccinfty  37419  bj-minftyccb  37430  finxpreclem2  37595  finxp0  37596  finxp1o  37597  finxpreclem3  37598  finxpreclem4  37599  finxpreclem5  37600  finxpreclem6  37601  poimirlem9  37830  poimirlem15  37836  poimirlem17  37838  poimirlem20  37841  poimirlem24  37845  poimirlem28  37849  mblfinlem2  37859  heiborlem6  38017  heiborlem7  38018  heiborlem8  38019  grposnOLD  38083  rngosn3  38125  gidsn  38153  zrdivrng  38154  brxrn  38568  ecxrn2  38593  br1cossxrnres  38711  dvhvaddval  41350  dvhvscaval  41359  dibglbN  41426  dihglbcpreN  41560  dihmeetlem4preN  41566  dihmeetlem13N  41579  hdmapfval  42087  elcnvlem  43842  cotrintab  43855  elimaint  43890  snhesn  44027  nregmodellem  45257  projf1o  45441  dvnprodlem1  46190  dvnprodlem2  46191  sge0xp  46673  hoicvr  46792  hoicvrrex  46800  hoidmv1le  46838  hoi2toco  46851  ovnlecvr2  46854  ovolval5lem2  46897  fsetsnf1  47298  setsidel  47622  prproropf1olem3  47751  prproropf1olem4  47752  prproropreud  47755  isisubgr  48108  ushggricedg  48173  gpgusgralem  48302  gpgvtxedg0  48309  gpgvtxedg1  48310  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem2  48318  gpg5nbgrvtx13starlem3  48319  gpg3nbgrvtx0  48322  gpg3nbgrvtx0ALT  48323  gpg3nbgrvtx1  48324  gpg5nbgrvtx03star  48326  gpg5nbgr3star  48327  gpg3kgrtriex  48335  gpgprismgr4cycllem2  48342  gpgprismgr4cycllem6  48346  gpgprismgr4cycllem7  48347  gpgprismgr4cycllem10  48350  gpg5edgnedg  48376  lmod1lem2  48734  lmod1lem3  48735  lmod1zr  48739  zlmodzxznm  48743  zlmodzxzldeplem  48744  rrx2xpref1o  48964  line2x  49000  inlinecirc02plem  49032  iinxp  49076  ovsng  49103  eloprab1st2nd  49113  tposid  49130  tposidres  49131  initc  49336  rescofuf  49338  idfurcl  49343  imaf1hom  49353  oppffn  49369  oppfvalg  49371  swapfval  49507  swapf1a  49514  swapf2a  49516  swapf1  49517  swapf2  49519  fucofvalg  49563  fucofval  49564  fucofvalne  49570  fuco21  49581  fucof21  49592  prcofvalg  49621  prcofvala  49622  prcofval  49623  thincciso  49698  setc1ocofval  49739  functermceu  49755  termcfuncval  49777  fucterm  49787  0fucterm  49788  relran  49869  ranval3  49876  ranrcl4lem  49883  ranup  49887  initocmd  49914