Theorem exbidv 1874

Description: Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-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-17 1575	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1663	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 105  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1877  2exbidv  1917  3exbidv  1918  eubidh  2086  eubid  2087  eleq1w  2293  eleq2w  2294  eleq1  2295  eleq2  2296  rexbidv2  2545  ceqsex2  2855  alexeq  2943  ceqex  2944  sbc5  3066  sbcex2  3096  sbcexg  3097  sbcabel  3125  eluni  3917  csbunig  3922  intab  3978  cbvopab1  4183  cbvopab1s  4185  axsep2  4229  zfauscl  4230  bnd2  4286  mss  4342  opeqex  4366  euotd  4371  snnex  4569  uniuni  4572  regexmid  4657  reg2exmid  4658  onintexmid  4695  reg3exmid  4702  nnregexmid  4743  opeliunxp  4805  csbxpg  4831  brcog  4922  elrn2g  4945  dfdmf  4949  csbdmg  4950  eldmg  4951  dfrnf  4998  elrn2  4999  elrnmpt1  5008  brcodir  5150  xp11m  5201  xpimasn  5211  csbrng  5224  elxp4  5250  elxp5  5251  dfco2a  5263  cores  5266  funimaexglem  5439  brprcneu  5663  ssimaexg  5739  dmfco  5745  fndmdif  5783  fmptco  5843  fliftf  5972  acexmidlem2  6047  acexmidlemv  6048  cbvoprab1  6125  cbvoprab2  6126  oprssdmm  6365  dmtpos  6487  tfrlemi1  6563  tfr1onlemaccex  6579  tfrcllemaccex  6592  ecdmn0m  6811  ereldm  6812  elqsn0m  6837  mapsnd  6923  mapsn  6925  breng  6982  bren  6983  brdom2g  6984  brdomg  6985  domeng  6989  mapsnend  7052  en2  7065  ac6sfi  7155  ordiso  7327  ctssdclemr  7403  enumct  7406  ctssexmid  7441  sspw1or2  7495  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  acneq  7509  finacn  7511  acfun  7514  ccfunen  7578  cc1  7579  cc2lem  7580  cc2  7581  cc3  7582  acnccim  7586  recexnq  7705  prarloc  7818  genpdflem  7822  genpassl  7839  genpassu  7840  ltexprlemell  7913  ltexprlemelu  7914  ltexprlemm  7915  recexprlemell  7937  recexprlemelu  7938  cnm  8147  sup3exmid  9231  seq3f1olemp  10877  zfz1isolem1  11212  zfz1iso  11213  sumeq1  12040  sumeq2  12044  summodc  12069  fsum3  12073  fsum2dlemstep  12120  ntrivcvgap0  12235  prodeq1f  12238  prodeq2w  12242  prodeq2  12243  prodmodc  12264  zproddc  12265  fprodseq  12269  fprodntrivap  12270  fprod2dlemstep  12308  ctinf  13181  ctiunct  13191  ssomct  13196  ptex  13477  igsumvalx  13602  gsumpropd  13605  gsumpropd2  13606  gsumress  13608  gsum0g  13609  islssm  14505  islssmg  14506  znleval  14801  uhgrm  16073  lpvtx  16074  incistruhgr  16085  upgrex  16098  uhgredgm  16131  subgruhgredgdm  16265  1loopgrvd2fi  16300  wlkm  16334  bdsep2  16656  bdzfauscl  16660  strcoll2  16753  sscoll2  16758  subctctexmid  16774  domomsubct  16775  nninfall  16787  gfsumval  16862