Theorem exbidv 1925

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

Syntax hints:   → wi 4   ↔ wb 205  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  nfbidv  1926  2exbidv  1928  3exbidv  1929  eleq1w  2817  eleq2w  2818  eleq1d  2819  eleq2dALT  2821  clelab  2880  nfcriOLD  2894  rexbidv2  3175  rmoeq1  3415  cgsex4gOLD  3522  ceqsex2  3530  ceqsex2v  3531  alexeqg  3640  sbc2or  3787  sbc5ALT  3807  sbcex2  3843  sbcabel  3873  elpreqprlem  4867  elpreqpr  4868  eluni  4912  csbuni  4941  intab  4983  cbvopab1  5224  cbvopab1g  5225  cbvopab1s  5227  cbvopab1v  5228  axrep1  5287  axreplem  5288  zfrepclf  5295  axsepg  5301  zfauscl  5302  sels  5439  euotd  5514  opeliunxp  5744  brcog  5867  elrn2g  5891  dfdmf  5897  eldmg  5899  dmopabelb  5917  dmopab2rex  5918  dfrnf  5950  elrnmpt1  5958  brcodir  6121  dfco2a  6246  cores  6249  sbcfung  6573  brprcneu  6882  brprcneuALT  6883  ssimaexg  6978  dmfco  6988  fndmdif  7044  fmptco  7127  fliftf  7312  imaeqsexv  7360  oprabbidv  7475  cbvoprab1  7496  cbvoprab2  7497  imaeqexov  7645  uniuni  7749  dmtpos  8223  frecseq123  8267  csbfrecsg  8269  frrlem1  8271  frrlem13  8283  wrecseq123OLD  8300  wfrlem1OLD  8308  wfrlem3OLDa  8311  wfrlem15OLD  8323  rdglim2  8432  ecdmn0  8750  mapsnd  8880  breng  8948  brenOLD  8950  brdom2g  8951  brdomgOLD  8953  domeng  8958  mapsnend  9036  isinf  9260  isinfOLD  9261  ac6sfi  9287  ordiso  9511  brwdom  9562  brwdom2  9568  zfregcl  9589  inf0  9616  zfinf  9634  ttrcleq  9704  brttrcl  9708  brttrcl2  9709  ssttrcl  9710  ttrcltr  9711  ttrclss  9715  ttrclselem2  9721  bnd2  9888  isinffi  9987  acneq  10038  acni  10040  aceq0  10113  aceq3lem  10115  dfac3  10116  dfac5lem4  10121  dfac8  10130  dfac9  10131  kmlem1  10145  kmlem2  10146  kmlem8  10152  kmlem10  10154  kmlem13  10157  cfval  10242  cardcf  10247  cfeq0  10251  cfsuc  10252  cff1  10253  cflim3  10257  cofsmo  10264  isfin4  10292  axcc2lem  10431  axcc4dom  10436  domtriomlem  10437  dcomex  10442  axdc2lem  10443  axdc4lem  10450  zfac  10455  ac7g  10469  ac4c  10471  ac5  10472  ac6sg  10483  weth  10490  axrepndlem1  10587  axunndlem1  10590  zfcndrep  10609  zfcndinf  10613  zfcndac  10614  gruina  10813  grothomex  10824  genpass  11004  1idpr  11024  ltexprlem3  11033  ltexprlem4  11034  ltexpri  11038  reclem2pr  11043  reclem3pr  11044  recexpr  11046  infm3  12173  nnunb  12468  axdc4uz  13949  ishashinf  14424  relexpindlem  15010  sumeq1  15635  sumeq2w  15638  sumeq2ii  15639  summo  15663  fsum  15666  fsum2dlem  15716  ntrivcvgn0  15844  ntrivcvgmullem  15847  prodeq1f  15852  prodeq2w  15856  prodeq2ii  15857  prodmo  15880  zprod  15881  fprod  15885  fprodntriv  15886  fprod2dlem  15924  vdwapun  16907  vdwmc  16911  vdwmc2  16912  isacs  17595  dfiso2  17719  brssc  17761  isssc  17767  equivestrcsetc  18104  dirge  18556  gsumvalx  18595  gsumpropd  18597  gsumpropd2lem  18598  gsumress  18601  gsumval3eu  19772  gsumval3lem2  19774  dprd2d2  19914  znleval  21110  neitr  22684  cmpcovf  22895  hausmapdom  23004  ptval  23074  elpt  23076  ptpjopn  23116  ptclsg  23119  ptcnp  23126  uffix2  23428  cnextf  23570  prdsxmslem2  24038  metustfbas  24066  metcld2  24824  dchrmusumlema  26996  dchrisum0lema  27017  elold  27365  lrrecfr  27429  istrkgld  27741  uvtx01vtx  28685  1loopgrvd2  28791  wspthsn  29133  iswspthn  29134  wspthsnon  29137  iswspthsnon  29141  wspthnon  29143  wlkiswwlks2  29160  wlkiswwlksupgr2  29162  wlklnwwlkln2lem  29167  wlksnwwlknvbij  29193  wspthsnwspthsnon  29201  elwwlks2on  29244  elwwlks2  29251  elwspths2spth  29252  clwlkclwwlk  29286  clwwlkvbij  29397  isgrpo  29781  adjeu  31173  iunrnmptss  31828  fcoinvbr  31867  2ndresdju  31905  fmptcof2  31913  acunirnmpt  31915  acunirnmpt2  31916  acunirnmpt2f  31917  aciunf1  31919  fnpreimac  31927  fpwrelmapffslem  31988  fmcncfil  32942  bnj865  33965  bnj1388  34075  bnj1489  34098  fineqvrep  34126  fineqvac  34128  satfrnmapom  34392  satf0op  34399  dmopab3rexdif  34427  prv1n  34453  eldm3  34762  opelco3  34777  elsingles  34921  funpartlem  34945  dfrdg4  34954  linedegen  35146  finminlem  35251  filnetlem4  35314  mobidvALT  35784  bj-issetwt  35802  bj-restuni  36026  bj-finsumval0  36214  csboprabg  36259  topdifinffinlem  36276  cbveud  36301  wl-sb8eut  36490  sdclem1  36659  fdc  36661  ismgmOLD  36766  isriscg  36900  elrnres  37187  eldm4  37190  exan3  37211  exanres  37212  eldmcnv  37262  brxrn  37292  cosseq  37344  brcoss  37349  brcoss3  37351  eldm1cossres  37378  brcosscnv  37390  islshpat  37935  lshpsmreu  38027  isopos  38098  islpln5  38454  islvol5  38498  pmapjat1  38772  dibelval3  40066  diblsmopel  40090  mapdpglem3  40594  hdmapglem7a  40846  19.9dev  41077  dfac11  41852  nnoeomeqom  42110  clcnvlem  42422  dfhe3  42574  ntrneineine0lem  42882  iotasbc  43226  iotasbc2  43227  fnchoice  43761  axccdom  43969  axccd  43976  stoweidlem35  44799  stoweidlem39  44803  dfatdmfcoafv2  46010  dfatco  46012  ichexmpl1  46185  ichnreuop  46188  ichreuopeq  46189  elsprel  46191  isomgr  46539  isomgreqve  46541  isomushgr  46542  isomuspgr  46550  isomgrsym  46552  isomgrtr  46555  ushrisomgr  46557  opeliun2xp  47056  map0cor  47569  thinccic  47729  bnd2d  47774