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  27364  lrrecfr  27427  istrkgld  27710  uvtx01vtx  28654  1loopgrvd2  28760  wspthsn  29102  iswspthn  29103  wspthsnon  29106  iswspthsnon  29110  wspthnon  29112  wlkiswwlks2  29129  wlkiswwlksupgr2  29131  wlklnwwlkln2lem  29136  wlksnwwlknvbij  29162  wspthsnwspthsnon  29170  elwwlks2on  29213  elwwlks2  29220  elwspths2spth  29221  clwlkclwwlk  29255  clwwlkvbij  29366  isgrpo  29750  adjeu  31142  iunrnmptss  31797  fcoinvbr  31836  2ndresdju  31874  fmptcof2  31882  acunirnmpt  31884  acunirnmpt2  31885  acunirnmpt2f  31886  aciunf1  31888  fnpreimac  31896  fpwrelmapffslem  31957  fmcncfil  32911  bnj865  33934  bnj1388  34044  bnj1489  34067  fineqvrep  34095  fineqvac  34097  satfrnmapom  34361  satf0op  34368  dmopab3rexdif  34396  prv1n  34422  eldm3  34731  opelco3  34746  elsingles  34890  funpartlem  34914  dfrdg4  34923  linedegen  35115  finminlem  35203  filnetlem4  35266  mobidvALT  35736  bj-issetwt  35754  bj-restuni  35978  bj-finsumval0  36166  csboprabg  36211  topdifinffinlem  36228  cbveud  36253  wl-sb8eut  36442  sdclem1  36611  fdc  36613  ismgmOLD  36718  isriscg  36852  elrnres  37139  eldm4  37142  exan3  37163  exanres  37164  eldmcnv  37214  brxrn  37244  cosseq  37296  brcoss  37301  brcoss3  37303  eldm1cossres  37330  brcosscnv  37342  islshpat  37887  lshpsmreu  37979  isopos  38050  islpln5  38406  islvol5  38450  pmapjat1  38724  dibelval3  40018  diblsmopel  40042  mapdpglem3  40546  hdmapglem7a  40798  19.9dev  41029  dfac11  41804  nnoeomeqom  42062  clcnvlem  42374  dfhe3  42526  ntrneineine0lem  42834  iotasbc  43178  iotasbc2  43179  fnchoice  43713  axccdom  43921  axccd  43928  stoweidlem35  44751  stoweidlem39  44755  dfatdmfcoafv2  45962  dfatco  45964  ichexmpl1  46137  ichnreuop  46140  ichreuopeq  46141  elsprel  46143  isomgr  46491  isomgreqve  46493  isomushgr  46494  isomuspgr  46502  isomgrsym  46504  isomgrtr  46507  ushrisomgr  46509  opeliun2xp  47008  map0cor  47521  thinccic  47681  bnd2d  47726