Theorem opex 5359

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 4803	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5336	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5214	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4518	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2912	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 398   ∈ wcel 2113  Vcvv 3497  ∅c0 4294  ifcif 4470  {csn 4570  {cpr 4572  ⟨cop 4576

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577

This theorem is referenced by:  otex  5360  brv  5367  otth2  5378  otthg  5380  sbcop1  5382  oteqex2  5392  oteqex  5393  snopeqop  5399  propeqop  5400  propssopi  5401  euop2  5405  opabidw  5415  opabid  5416  elopab  5417  rexopabb  5418  opabn0  5443  opeliunxp  5622  elvvv  5630  opbrop  5651  relsnopg  5679  xpiindi  5709  raliunxp  5713  idrefALT  5976  intirr  5981  xpnz  6019  dmsnn0  6067  dmsnopg  6073  cnvcnvsn  6079  op2ndb  6087  opswap  6089  cnviin  6140  reuop  6147  funopg  6392  dffv2  6759  fsn  6900  f1o2sn  6907  idref  6911  funsndifnop  6916  fmptsng  6933  fmptsnd  6934  fvsng  6945  resfunexg  6981  fveqf1o  7061  fliftel  7065  fliftel1  7066  oprabidw  7190  oprabid  7191  dfoprab2  7215  oprabv  7217  rnoprab  7260  eloprabga  7264  ot1stg  7706  ot2ndg  7707  ot3rdg  7708  fo1st  7712  fo2nd  7713  br1steqg  7714  br2ndeqg  7715  opiota  7760  eloprabi  7764  mposn  7801  fpar  7814  fsplitfpar  7817  algrflem  7822  frxp  7823  xporderlem  7824  fnwelem  7828  fvproj  7831  fimaproj  7832  mpoxopoveq  7888  brtpos  7904  dmtpos  7907  rntpos  7908  tpostpos  7915  wfrlem14  7971  tfrlem11  8027  seqomlem1  8089  seqomlem3  8091  seqomlem4  8092  omeu  8214  iiner  8372  xpsnen  8604  xpcomco  8610  xpassen  8614  xpmapenlem  8687  unxpdomlem1  8725  inlresf  9346  inrresf  9348  djur  9351  djuss  9352  djuun  9358  1stinl  9359  2ndinl  9360  1stinr  9361  2ndinr  9362  fseqenlem2  9454  dju1dif  9601  fpwwe  10071  addpipq2  10361  addpqnq  10363  mulpipq2  10364  mulpqnq  10366  ordpipq  10367  prlem934  10458  addcnsr  10560  mulcnsr  10561  ltresr  10565  addcnsrec  10568  mulcnsrec  10569  axcnre  10589  om2uzrdg  13327  uzrdg0i  13330  uzrdgsuci  13331  hashfun  13801  wrdexb  13876  s1len  13963  s1nz  13964  s111  13972  wrdlen2i  14307  brintclab  14364  fsumcnv  15131  fprodcnv  15340  ruclem1  15587  ruclem4  15590  eucalgval2  15928  crth  16118  phimullem  16119  setsval  16516  setsdm  16520  setsfun  16521  setsfun0  16522  setsexstruct2  16525  setsres  16528  setscom  16530  strfv  16534  setsid  16541  imasaddfnlem  16804  imasaddvallem  16805  imasvscafn  16813  idfuval  17149  cofuval  17155  resfval  17165  resfval2  17166  elhoma  17295  embedsetcestrclem  17410  xpcco  17436  xpcid  17442  1stfval  17444  2ndfval  17447  prfval  17452  prf1  17453  prf2  17455  evlfval  17470  curfval  17476  curf1  17478  curfcl  17485  hofval  17505  intopsn  17867  mgm1  17871  sgrp1  17913  mnd1  17955  mnd1id  17956  grpss  18124  grp1  18209  symg2bas  18524  efgmval  18841  efgi  18848  efgi2  18854  frgpnabllem1  18996  frgpnabllem2  18997  ring1  19355  opsrtoslem2  20268  mat1dimelbas  21083  mat1dimbas  21084  mat1dimscm  21087  mat1dimmul  21088  mat1f1o  21090  mat1rhmelval  21092  mvmulfval  21154  m2detleib  21243  txcnp  22231  upxp  22234  uptx  22236  txdis1cn  22246  hauseqlcld  22257  txlm  22259  xkoinjcn  22298  txflf  22617  qustgplem  22732  ucnima  22893  ucnprima  22894  fmucndlem  22903  imasdsf1olem  22986  cnheiborlem  23561  ovollb2lem  24092  ovolctb  24094  ovolshftlem1  24113  ovolscalem1  24117  ovolicc1  24120  ioombl1lem3  24164  ioombl1lem4  24165  ioorval  24178  dyadval  24196  mbfimaopnlem  24259  limccnp2  24493  brbtwn  26688  brcgr  26689  eengbas  26770  ebtwntg  26771  ecgrtg  26772  elntg  26773  structvtxval  26809  structgrssvtx  26812  structgrssiedg  26813  gropd  26819  isuhgrop  26858  uhgrunop  26863  upgrop  26882  upgr0eop  26902  upgrunop  26907  umgrunop  26909  isuspgrop  26949  isusgrop  26950  ausgrusgrb  26953  usgr0eop  27031  usgrexmpl  27048  griedg0ssusgr  27050  uhgrspanop  27081  uhgrspan1  27088  upgrres  27091  umgrres  27092  usgrres  27093  upgrres1  27098  umgrres1  27099  usgrres1  27100  usgrexi  27226  cusgrexi  27228  cffldtocusgr  27232  cusgrres  27233  vtxdgop  27255  umgr2v2e  27310  wlkp1lem2  27459  wlkswwlksf1o  27660  wwlksnext  27674  eupth2eucrct  27999  eupthvdres  28017  konigsbergumgr  28033  numclwwlk1lem2fv  28138  numclwlk1lem1  28151  ex-br  28213  ex-fpar  28244  cnnvg  28458  cnnvs  28460  cnnvnm  28461  h2hva  28754  h2hsm  28755  h2hnm  28756  hhssva  29037  hhsssm  29038  hhssnm  29039  hhshsslem1  29047  br8d  30364  xppreima2  30398  aciunf1lem  30410  ofpreima  30413  brsnop  30432  cnvoprabOLD  30459  linds2eq  30945  smatrcl  31065  smatlem  31066  txomap  31102  qtophaus  31104  hgt750lemb  31931  bnj97  32142  bnj553  32174  bnj966  32220  bnj1442  32325  erdszelem9  32450  erdszelem10  32451  txpconn  32483  txsconnlem  32491  goel  32598  goeleq12bg  32600  gonafv  32601  gonanegoal  32603  sat1el2xp  32630  fmlaomn0  32641  gonan0  32643  goaln0  32644  gonarlem  32645  gonar  32646  goalrlem  32647  goalr  32648  fmla0disjsuc  32649  fmlasucdisj  32650  satffunlem  32652  satffunlem1lem1  32653  satffunlem2lem1  32655  satfv0fvfmla0  32664  sategoelfvb  32670  prv1n  32682  msubval  32776  mvhval  32785  msubvrs  32811  brtpid1  32955  brtpid2  32956  brtpid3  32957  brtp  32989  dfpo2  32995  br8  32996  br6  32997  br4  32998  dfdm5  33020  dfrn5  33021  elima4  33023  fv1stcnv  33024  fv2ndcnv  33025  brtxp  33345  brpprod  33350  brpprod3b  33352  brsset  33354  brtxpsd  33359  dffun10  33379  elfuns  33380  brcart  33397  brimg  33402  brapply  33403  brcup  33404  brcap  33405  brsuccf  33406  brrestrict  33414  dfrecs2  33415  dfrdg4  33416  fvtransport  33497  brcolinear2  33523  colineardim1  33526  brsegle  33573  fvline  33609  ellines  33617  filnetlem3  33732  bj-inftyexpitaufo  34488  bj-inftyexpitaudisj  34491  bj-inftyexpiinv  34494  bj-inftyexpidisj  34496  bj-elccinfty  34500  bj-minftyccb  34511  finxpreclem2  34675  finxp0  34676  finxp1o  34677  finxpreclem3  34678  finxpreclem4  34679  finxpreclem5  34680  finxpreclem6  34681  poimirlem9  34905  poimirlem15  34911  poimirlem17  34913  poimirlem20  34916  poimirlem24  34920  poimirlem28  34924  mblfinlem2  34934  heiborlem6  35098  heiborlem7  35099  heiborlem8  35100  grposnOLD  35164  rngosn3  35206  gidsn  35234  zrdivrng  35235  brxrn  35630  br1cossxrnres  35692  dvhvaddval  38230  dvhvscaval  38239  dibglbN  38306  dihglbcpreN  38440  dihmeetlem4preN  38446  dihmeetlem13N  38459  hdmapfval  38967  elcnvlem  39967  cotrintab  39980  elimaint  39999  snhesn  40138  projf1o  41465  dvnprodlem1  42237  dvnprodlem2  42238  sge0xp  42718  hoicvr  42837  hoicvrrex  42845  hoidmv1le  42883  hoi2toco  42896  ovnlecvr2  42899  ovolval5lem2  42942  setsidel  43543  prproropf1olem3  43674  prproropf1olem4  43675  prproropreud  43678  ushrisomgr  44013  opeliun2xp  44388  lmod1lem2  44550  lmod1lem3  44551  lmod1zr  44555  zlmodzxznm  44559  zlmodzxzldeplem  44560  rrx2xpref1o  44712  line2x  44748  inlinecirc02plem  44780