Theorem exbidv 1951

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1897 and exbid 2259. (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 1940	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1897	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  nfbidv  1952  2exbidv  1954  3exbidv  1955  eleq1w  2846  eleq2w  2847  eleq1d  2848  eleq2dALT  2850  clelab  2907  rexbidv2  3185  rmoeq1  3400  ceqsex2  3505  ceqsex2v  3506  alexeqg  3610  sbc2or  3753  sbc5ALT  3773  sbcex2  3804  sbcabel  3831  elpreqprlem  4831  elpreqpr  4832  eluni  4875  csbuni  4903  intab  4943  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  cbvopab1v  5189  axrep1  5239  axreplem  5240  zfrepclf  5252  axsepg  5258  sepg  5259  zfausclOLD  5261  sels  5421  euotd  5496  opeliunxp  5728  opeliun2xp  5729  brcog  5852  elrn2g  5880  dfdmf  5886  eldmg  5888  dmun  5900  dmopabelb  5906  dmopab2rex  5907  dm0rn0  5914  dfrnf  5940  elrnmpt1  5950  brcodir  6119  dfco2a  6247  cores  6250  sbcfung  6560  brprcneu  6871  brprcneuALT  6872  ssimaexg  6967  dmfco  6977  fndmdif  7037  fmptco  7125  fliftf  7313  imaeqsexvOLD  7361  oprabbidv  7476  cbvoprab1  7497  cbvoprab2  7498  cbvoprab12v  7500  imaeqexov  7648  uniuni  7757  dmtpos  8230  frecseq123  8275  csbfrecsg  8277  frrlem1  8279  frrlem13  8291  rdglim2  8415  ecdmn0  8743  mapsnd  8880  breng  8948  brdom2g  8950  domeng  8955  mapsnend  9029  isinf  9221  ac6sfi  9240  ordiso  9474  brwdom  9525  brwdom2  9531  zfregcl  9552  zfregclOLD  9553  inf0  9586  zfinf  9604  ttrcleq  9674  brttrcl  9678  brttrcl2  9679  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  bnd2  9875  isinffi  9974  acneq  10023  acni  10025  aceq0  10098  aceq3lem  10100  dfac3  10101  dfac5lem4  10106  dfac8  10115  dfac9  10116  kmlem1  10130  kmlem2  10131  kmlem8  10137  kmlem10  10139  kmlem13  10142  cfval  10225  cardcf  10230  cfeq0  10235  cfsuc  10236  cff1  10237  cflim3  10241  cofsmo  10248  isfin4  10276  axcc2lem  10415  axcc4dom  10420  domtriomlem  10421  dcomex  10426  axdc2lem  10427  axdc4lem  10434  zfac  10439  ac7g  10453  ac4c  10455  ac5  10456  ac6sg  10467  weth  10474  axrepndlem1  10572  axunndlem1  10575  zfcndrep  10594  zfcndinf  10598  zfcndac  10599  gruina  10798  grothomex  10809  genpass  10989  1idpr  11009  ltexprlem3  11018  ltexprlem4  11019  ltexpri  11023  reclem2pr  11028  reclem3pr  11029  recexpr  11031  infm3  12169  nnunb  12495  axdc4uz  14016  ishashinf  14496  relexpindlem  15096  sumeq1  15736  sumeq2w  15739  sumeq2ii  15740  sumeq2sdv  15750  summo  15764  fsum  15767  fsum2dlem  15817  ntrivcvgn0  15948  ntrivcvgmullem  15951  prodeq1f  15956  prodeq1  15957  prodeq2w  15960  prodeq2ii  15961  prodeq2sdv  15973  prodmo  15986  zprod  15987  fprod  15991  fprodntriv  15992  fprod2dlem  16030  vdwapun  17029  vdwmc  17033  vdwmc2  17034  isacs  17702  dfiso2  17824  brssc  17866  isssc  17872  equivestrcsetc  18203  dirge  18654  gsumvalx  18729  gsumpropd  18731  gsumpropd2lem  18732  gsumress  18735  gsumval3eu  19969  gsumval3lem2  19971  dprd2d2  20111  znleval  21704  neitr  23337  cmpcovf  23548  hausmapdom  23657  ptval  23727  elpt  23729  ptpjopn  23769  ptclsg  23772  ptcnp  23779  uffix2  24081  cnextf  24223  prdsxmslem2  24686  metustfbas  24714  metcld2  25466  dchrmusumlema  27657  dchrisum0lema  27678  elold  28052  lrrecfr  28136  istrkgld  28728  uvtx01vtx  29747  1loopgrvd2  29853  wspthsn  30197  iswspthn  30198  wspthsnon  30201  iswspthsnon  30205  wspthnon  30207  wlkiswwlks2  30224  wlkiswwlksupgr2  30226  wlklnwwlkln2lem  30231  wlksnwwlknvbij  30257  wspthsnwspthsnon  30265  elwwlks2on  30310  elwwlks2  30318  elwspths2spth  30319  clwlkclwwlk  30353  clwwlkvbij  30464  isgrpo  30849  adjeu  32241  iunrnmptss  32910  fcoinvbr  32950  2ndresdju  32994  fmptcof2  33002  acunirnmpt  33004  acunirnmpt2  33005  acunirnmpt2f  33006  aciunf1  33008  fnpreimac  33015  fpwrelmapffslem  33077  gsumwrd2dccatlem  33397  1arithidomlem1  33825  1arithidom  33827  fmcncfil  34321  bnj865  35311  bnj1388  35421  bnj1489  35444  fineqvrep  35527  fineqvac  35529  tz9.1regs  35547  satfrnmapom  35862  satf0op  35869  dmopab3rexdif  35897  prv1n  35923  rexxfr3dALT  36131  eldm3  36253  opelco3  36267  elsingles  36408  funpartlem  36434  dfrdg4  36443  linedegen  36635  prodeq12sdv  36750  cbvoprab2vw  36770  cbvoprab13vw  36773  cbvmodavw  36782  cbvopab1davw  36796  cbvopab2davw  36797  cbvoprab2davw  36804  cbvoprab12davw  36807  cbvoprab23davw  36808  cbvoprab13davw  36809  cbvsumdavw  36811  cbvproddavw  36812  cbvsumdavw2  36827  cbvproddavw2  36828  finminlem  36849  filnetlem4  36912  axtco1  37004  axtco1from2  37006  axtco1g  37007  dfttc4lem1  37059  dfttc4  37061  elttcirr  37062  ttcexg  37063  regsfromregtco  37069  mh-regprimbi  37076  mh-infprim1bi  37077  mobidvALT  37512  bj-issetwt  37530  bj-inex1gALT  37580  bj-axreprepsep  37732  bj-restuni  37759  bj-finsumval0  37949  csboprabg  37996  topdifinffinlem  38013  cbveud  38038  wl-sb8eut  38253  wl-sb8eutv  38254  sdclem1  38414  fdc  38416  ismgmOLD  38521  isriscg  38655  elrnres  38947  eldm4  38950  exan3  38969  exanres  38970  eldmcnv  39014  brxrn  39052  exeupre  39160  cosseq  39185  brcoss  39190  brcoss3  39192  eldm1cossres  39219  brcosscnv  39231  islshpat  39811  lshpsmreu  39903  isopos  39974  islpln5  40329  islvol5  40373  pmapjat1  40647  dibelval3  41941  diblsmopel  41965  mapdpglem3  42469  hdmapglem7a  42721  19.9dev  43006  fimgmcyc  43322  dfac11  43809  nnoeomeqom  44059  clcnvlem  44369  dfhe3  44521  ntrneineine0lem  44829  iotasbc  45149  iotasbc2  45150  brpermmodel  45732  permaxinf2lem  45741  permac8prim  45743  nregmodel  45746  fnchoice  45769  axccdom  45958  axccd  45964  stoweidlem35  46769  stoweidlem39  46773  dfatdmfcoafv2  48011  dfatco  48013  ichexmpl1  48238  ichnreuop  48241  ichreuopeq  48242  elsprel  48244  isgrim  48667  dfgric2  48700  gricushgr  48702  gricuspgr  48703  ushggricedg  48712  isubgrgrim  48714  uhgrimisgrgric  48716  grtri  48725  grtriprop  48726  isgrtri  48728  uspgrlim  48777  grlimedgclnbgr  48780  grlimgrtri  48788  dfgrlic2  48793  dfgrlic3  48795  grilcbri2  48796  map0cor  49653  nelsubc3lem  49868  thinccic  50269  istermc  50272  termcpropd  50301  discsntermlem  50368  basrestermcfolem  50369  discsnterm  50372  cnelsubclem  50401  bnd2d  50479