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  3797  csbunig  3802  intab  3858  cbvopab1  4060  cbvopab1s  4062  axsep2  4106  zfauscl  4107  bnd2  4157  mss  4209  opeqex  4232  euotd  4237  snnex  4431  uniuni  4434  regexmid  4517  reg2exmid  4518  onintexmid  4555  reg3exmid  4562  nnregexmid  4603  opeliunxp  4664  csbxpg  4690  brcog  4776  elrn2g  4799  dfdmf  4802  csbdmg  4803  eldmg  4804  dfrnf  4850  elrn2  4851  elrnmpt1  4860  brcodir  4996  xp11m  5047  xpimasn  5057  csbrng  5070  elxp4  5096  elxp5  5097  dfco2a  5109  cores  5112  funimaexglem  5279  brprcneu  5487  ssimaexg  5556  dmfco  5562  fndmdif  5598  fmptco  5659  fliftf  5775  acexmidlem2  5847  acexmidlemv  5848  cbvoprab1  5922  cbvoprab2  5923  oprssdmm  6147  dmtpos  6232  tfrlemi1  6308  tfr1onlemaccex  6324  tfrcllemaccex  6337  ecdmn0m  6551  ereldm  6552  elqsn0m  6577  mapsn  6664  bren  6721  brdomg  6722  domeng  6726  ac6sfi  6872  ordiso  7009  ctssdclemr  7085  enumct  7088  ctssexmid  7122  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  acfun  7171  ccfunen  7213  cc1  7214  cc2lem  7215  cc2  7216  cc3  7217  recexnq  7339  prarloc  7452  genpdflem  7456  genpassl  7473  genpassu  7474  ltexprlemell  7547  ltexprlemelu  7548  ltexprlemm  7549  recexprlemell  7571  recexprlemelu  7572  cnm  7781  sup3exmid  8860  seq3f1olemp  10445  zfz1isolem1  10762  zfz1iso  10763  sumeq1  11305  sumeq2  11309  summodc  11333  fsum3  11337  fsum2dlemstep  11384  ntrivcvgap0  11499  prodeq1f  11502  prodeq2w  11506  prodeq2  11507  prodmodc  11528  zproddc  11529  fprodseq  11533  fprodntrivap  11534  fprod2dlemstep  11572  ctinf  12372  ctiunct  12382  ssomct  12387  bdsep2  13843  bdzfauscl  13847  strcoll2  13940  sscoll2  13945  subctctexmid  13956  nninfall  13964