Theorem exbidv 1928

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1874 and exbid 2235. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
exbidv	⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem exbidv

Step	Hyp	Ref	Expression
1		ax-5 1917	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1874	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 207  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  nfbidv  1929  2exbidv  1931  3exbidv  1932  eleq1w  2822  eleq2w  2823  eleq1d  2824  eleq2dALT  2826  clelab  2883  rexbidv2  3159  rmoeq1  3375  ceqsex2  3482  ceqsex2v  3483  alexeqg  3589  sbc2or  3732  sbc5ALT  3752  sbcex2  3783  sbcabel  3810  elpreqprlem  4797  elpreqpr  4798  eluni  4841  csbuni  4868  intab  4908  cbvopab1  5146  cbvopab1g  5147  cbvopab1s  5149  cbvopab1v  5150  axrep1  5200  axreplem  5201  zfrepclf  5213  axsepg  5219  zfauscl  5220  sels  5379  euotd  5454  opeliunxp  5685  opeliun2xp  5686  brcog  5808  elrn2g  5832  dfdmf  5838  eldmg  5840  dmun  5852  dmopabelb  5858  dmopab2rex  5859  dm0rn0  5866  dfrnf  5892  elrnmpt1  5902  brcodir  6069  dfco2a  6197  cores  6200  sbcfung  6509  brprcneu  6817  brprcneuALT  6818  ssimaexg  6913  dmfco  6923  fndmdif  6983  fmptco  7071  fliftf  7259  imaeqsexvOLD  7307  oprabbidv  7422  cbvoprab1  7443  cbvoprab2  7444  cbvoprab12v  7446  imaeqexov  7594  uniuni  7705  dmtpos  8178  frecseq123  8222  csbfrecsg  8224  frrlem1  8226  frrlem13  8238  rdglim2  8361  ecdmn0  8686  mapsnd  8824  breng  8892  brdom2g  8894  domeng  8899  mapsnend  8973  isinf  9165  ac6sfi  9184  ordiso  9421  brwdom  9472  brwdom2  9478  zfregcl  9499  zfregclOLD  9500  inf0  9533  zfinf  9551  ttrcleq  9621  brttrcl  9625  brttrcl2  9626  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  bnd2  9808  isinffi  9907  acneq  9956  acni  9958  aceq0  10031  aceq3lem  10033  dfac3  10034  dfac5lem4  10039  dfac5lem4OLD  10041  dfac8  10049  dfac9  10050  kmlem1  10064  kmlem2  10065  kmlem8  10071  kmlem10  10073  kmlem13  10076  cfval  10160  cardcf  10165  cfeq0  10169  cfsuc  10170  cff1  10171  cflim3  10175  cofsmo  10182  isfin4  10210  axcc2lem  10349  axcc4dom  10354  domtriomlem  10355  dcomex  10360  axdc2lem  10361  axdc4lem  10368  zfac  10373  ac7g  10387  ac4c  10389  ac5  10390  ac6sg  10401  weth  10408  axrepndlem1  10506  axunndlem1  10509  zfcndrep  10528  zfcndinf  10532  zfcndac  10533  gruina  10732  grothomex  10743  genpass  10923  1idpr  10943  ltexprlem3  10952  ltexprlem4  10953  ltexpri  10957  reclem2pr  10962  reclem3pr  10963  recexpr  10965  infm3  12106  nnunb  12424  axdc4uz  13937  ishashinf  14416  relexpindlem  15016  sumeq1  15642  sumeq2w  15645  sumeq2ii  15646  sumeq2sdv  15656  summo  15670  fsum  15673  fsum2dlem  15723  ntrivcvgn0  15854  ntrivcvgmullem  15857  prodeq1f  15862  prodeq1  15863  prodeq2w  15866  prodeq2ii  15867  prodeq2sdv  15879  prodmo  15892  zprod  15893  fprod  15897  fprodntriv  15898  fprod2dlem  15936  vdwapun  16936  vdwmc  16940  vdwmc2  16941  isacs  17608  dfiso2  17730  brssc  17772  isssc  17778  equivestrcsetc  18109  dirge  18560  gsumvalx  18635  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  gsumval3eu  19870  gsumval3lem2  19872  dprd2d2  20012  znleval  21529  neitr  23163  cmpcovf  23374  hausmapdom  23483  ptval  23553  elpt  23555  ptpjopn  23595  ptclsg  23598  ptcnp  23605  uffix2  23907  cnextf  24049  prdsxmslem2  24512  metustfbas  24540  metcld2  25292  dchrmusumlema  27474  dchrisum0lema  27495  elold  27869  lrrecfr  27953  istrkgld  28545  uvtx01vtx  29484  1loopgrvd2  29590  wspthsn  29934  iswspthn  29935  wspthsnon  29938  iswspthsnon  29942  wspthnon  29944  wlkiswwlks2  29961  wlkiswwlksupgr2  29963  wlklnwwlkln2lem  29968  wlksnwwlknvbij  29994  wspthsnwspthsnon  30002  elwwlks2on  30047  elwwlks2  30055  elwspths2spth  30056  clwlkclwwlk  30090  clwwlkvbij  30201  isgrpo  30586  adjeu  31978  iunrnmptss  32654  fcoinvbr  32694  2ndresdju  32741  fmptcof2  32749  acunirnmpt  32751  acunirnmpt2  32752  acunirnmpt2f  32753  aciunf1  32755  fnpreimac  32762  fpwrelmapffslem  32824  gsumwrd2dccatlem  33158  1arithidomlem1  33618  1arithidom  33620  fmcncfil  34115  bnj865  35105  bnj1388  35215  bnj1489  35238  fineqvrep  35295  fineqvac  35297  tz9.1regs  35315  satfrnmapom  35598  satf0op  35605  dmopab3rexdif  35633  prv1n  35659  rexxfr3dALT  35867  eldm3  35989  opelco3  36003  elsingles  36144  funpartlem  36170  dfrdg4  36179  linedegen  36371  prodeq12sdv  36446  cbvoprab2vw  36466  cbvoprab13vw  36469  cbvmodavw  36478  cbvopab1davw  36492  cbvopab2davw  36493  cbvoprab2davw  36500  cbvoprab12davw  36503  cbvoprab23davw  36504  cbvoprab13davw  36505  cbvsumdavw  36507  cbvproddavw  36508  cbvsumdavw2  36523  cbvproddavw2  36524  finminlem  36546  filnetlem4  36609  axtco1  36701  axtco1from2  36703  axtco1g  36704  dfttc4lem1  36756  dfttc4  36758  elttcirr  36759  ttcexg  36760  regsfromregtco  36766  mh-regprimbi  36773  mh-infprim1bi  36774  mobidvALT  37210  bj-issetwt  37228  bj-axreprepsep  37428  bj-restuni  37455  bj-finsumval0  37645  csboprabg  37692  topdifinffinlem  37709  cbveud  37734  wl-sb8eut  37949  wl-sb8eutv  37950  sdclem1  38110  fdc  38112  ismgmOLD  38217  isriscg  38351  elrnres  38645  eldm4  38648  exan3  38667  exanres  38668  eldmcnv  38712  brxrn  38750  exeupre  38858  cosseq  38883  brcoss  38888  brcoss3  38890  eldm1cossres  38917  brcosscnv  38929  islshpat  39509  lshpsmreu  39601  isopos  39672  islpln5  40027  islvol5  40071  pmapjat1  40345  dibelval3  41639  diblsmopel  41663  mapdpglem3  42167  hdmapglem7a  42419  19.9dev  42702  fimgmcyc  43020  dfac11  43507  nnoeomeqom  43757  clcnvlem  44067  dfhe3  44219  ntrneineine0lem  44527  iotasbc  44863  iotasbc2  44864  brpermmodel  45447  permaxinf2lem  45456  permac8prim  45458  nregmodel  45461  fnchoice  45477  axccdom  45667  axccd  45673  stoweidlem35  46478  stoweidlem39  46482  dfatdmfcoafv2  47717  dfatco  47719  ichexmpl1  47944  ichnreuop  47947  ichreuopeq  47948  elsprel  47950  isgrim  48373  dfgric2  48406  gricushgr  48408  gricuspgr  48409  ushggricedg  48418  isubgrgrim  48420  uhgrimisgrgric  48422  grtri  48431  grtriprop  48432  isgrtri  48434  uspgrlim  48483  grlimedgclnbgr  48486  grlimgrtri  48494  dfgrlic2  48499  dfgrlic3  48501  grilcbri2  48502  map0cor  49345  nelsubc3lem  49560  thinccic  49961  istermc  49964  termcpropd  49993  discsntermlem  50060  basrestermcfolem  50061  discsnterm  50064  cnelsubclem  50093  bnd2d  50171