Theorem exbidv 1818

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 1519	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1607	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 104  ∃wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11ev  1821  2exbidv  1861  3exbidv  1862  eubidh  2025  eubid  2026  eleq1w  2231  eleq2w  2232  eleq1  2233  eleq2  2234  rexbidv2  2473  ceqsex2  2770  alexeq  2856  ceqex  2857  sbc5  2978  sbcex2  3008  sbcexg  3009  sbcabel  3036  eluni  3799  csbunig  3804  intab  3860  cbvopab1  4062  cbvopab1s  4064  axsep2  4108  zfauscl  4109  bnd2  4159  mss  4211  opeqex  4234  euotd  4239  snnex  4433  uniuni  4436  regexmid  4519  reg2exmid  4520  onintexmid  4557  reg3exmid  4564  nnregexmid  4605  opeliunxp  4666  csbxpg  4692  brcog  4778  elrn2g  4801  dfdmf  4804  csbdmg  4805  eldmg  4806  dfrnf  4852  elrn2  4853  elrnmpt1  4862  brcodir  4998  xp11m  5049  xpimasn  5059  csbrng  5072  elxp4  5098  elxp5  5099  dfco2a  5111  cores  5114  funimaexglem  5281  brprcneu  5489  ssimaexg  5558  dmfco  5564  fndmdif  5601  fmptco  5662  fliftf  5778  acexmidlem2  5850  acexmidlemv  5851  cbvoprab1  5925  cbvoprab2  5926  oprssdmm  6150  dmtpos  6235  tfrlemi1  6311  tfr1onlemaccex  6327  tfrcllemaccex  6340  ecdmn0m  6555  ereldm  6556  elqsn0m  6581  mapsn  6668  bren  6725  brdomg  6726  domeng  6730  ac6sfi  6876  ordiso  7013  ctssdclemr  7089  enumct  7092  ctssexmid  7126  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  acfun  7184  ccfunen  7226  cc1  7227  cc2lem  7228  cc2  7229  cc3  7230  recexnq  7352  prarloc  7465  genpdflem  7469  genpassl  7486  genpassu  7487  ltexprlemell  7560  ltexprlemelu  7561  ltexprlemm  7562  recexprlemell  7584  recexprlemelu  7585  cnm  7794  sup3exmid  8873  seq3f1olemp  10458  zfz1isolem1  10775  zfz1iso  10776  sumeq1  11318  sumeq2  11322  summodc  11346  fsum3  11350  fsum2dlemstep  11397  ntrivcvgap0  11512  prodeq1f  11515  prodeq2w  11519  prodeq2  11520  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodntrivap  11547  fprod2dlemstep  11585  ctinf  12385  ctiunct  12395  ssomct  12400  bdsep2  13921  bdzfauscl  13925  strcoll2  14018  sscoll2  14023  subctctexmid  14034  nninfall  14042