Theorem exbidv 1764

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11ev  1767  2exbidv  1807  3exbidv  1808  eubidh  1966  eubid  1967  eleq1w  2160  eleq2w  2161  eleq1  2162  eleq2  2163  rexbidv2  2399  ceqsex2  2681  alexeq  2765  ceqex  2766  sbc5  2885  sbcex2  2914  sbcexg  2915  sbcabel  2942  eluni  3686  csbunig  3691  intab  3747  cbvopab1  3941  cbvopab1s  3943  axsep2  3987  zfauscl  3988  bnd2  4037  mss  4086  opeqex  4109  euotd  4114  snnex  4307  uniuni  4310  regexmid  4388  reg2exmid  4389  onintexmid  4425  reg3exmid  4432  nnregexmid  4472  opeliunxp  4532  csbxpg  4558  brcog  4644  elrn2g  4667  dfdmf  4670  csbdmg  4671  eldmg  4672  dfrnf  4718  elrn2  4719  elrnmpt1  4728  brcodir  4862  xp11m  4913  xpimasn  4923  csbrng  4936  elxp4  4962  elxp5  4963  dfco2a  4975  cores  4978  funimaexglem  5142  brprcneu  5346  ssimaexg  5415  dmfco  5421  fndmdif  5457  fmptco  5518  fliftf  5632  acexmidlem2  5703  acexmidlemv  5704  cbvoprab1  5775  cbvoprab2  5776  dmtpos  6083  tfrlemi1  6159  tfr1onlemaccex  6175  tfrcllemaccex  6188  ecdmn0m  6401  ereldm  6402  elqsn0m  6427  mapsn  6514  bren  6571  brdomg  6572  domeng  6576  ac6sfi  6721  ordiso  6836  ctssdclemr  6911  enumct  6914  ctssexmid  6936  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  recexnq  7099  prarloc  7212  genpdflem  7216  genpassl  7233  genpassu  7234  ltexprlemell  7307  ltexprlemelu  7308  ltexprlemm  7309  recexprlemell  7331  recexprlemelu  7332  sup3exmid  8573  seq3f1olemp  10116  zfz1isolem1  10424  zfz1iso  10425  sumeq1  10963  sumeq2  10967  summodc  10991  fsum3  10995  fsum2dlemstep  11042  ctinf  11735  bdsep2  12665  bdzfauscl  12669  strcoll2  12766  nninfall  12788