Theorem exbidv 1825

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1828  2exbidv  1868  3exbidv  1869  eubidh  2032  eubid  2033  eleq1w  2238  eleq2w  2239  eleq1  2240  eleq2  2241  rexbidv2  2480  ceqsex2  2777  alexeq  2863  ceqex  2864  sbc5  2986  sbcex2  3016  sbcexg  3017  sbcabel  3044  eluni  3812  csbunig  3817  intab  3873  cbvopab1  4076  cbvopab1s  4078  axsep2  4122  zfauscl  4123  bnd2  4173  mss  4226  opeqex  4249  euotd  4254  snnex  4448  uniuni  4451  regexmid  4534  reg2exmid  4535  onintexmid  4572  reg3exmid  4579  nnregexmid  4620  opeliunxp  4681  csbxpg  4707  brcog  4794  elrn2g  4817  dfdmf  4820  csbdmg  4821  eldmg  4822  dfrnf  4868  elrn2  4869  elrnmpt1  4878  brcodir  5016  xp11m  5067  xpimasn  5077  csbrng  5090  elxp4  5116  elxp5  5117  dfco2a  5129  cores  5132  funimaexglem  5299  brprcneu  5508  ssimaexg  5578  dmfco  5584  fndmdif  5621  fmptco  5682  fliftf  5799  acexmidlem2  5871  acexmidlemv  5872  cbvoprab1  5946  cbvoprab2  5947  oprssdmm  6171  dmtpos  6256  tfrlemi1  6332  tfr1onlemaccex  6348  tfrcllemaccex  6361  ecdmn0m  6576  ereldm  6577  elqsn0m  6602  mapsn  6689  bren  6746  brdomg  6747  domeng  6751  ac6sfi  6897  ordiso  7034  ctssdclemr  7110  enumct  7113  ctssexmid  7147  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  acfun  7205  ccfunen  7262  cc1  7263  cc2lem  7264  cc2  7265  cc3  7266  recexnq  7388  prarloc  7501  genpdflem  7505  genpassl  7522  genpassu  7523  ltexprlemell  7596  ltexprlemelu  7597  ltexprlemm  7598  recexprlemell  7620  recexprlemelu  7621  cnm  7830  sup3exmid  8913  seq3f1olemp  10501  zfz1isolem1  10819  zfz1iso  10820  sumeq1  11362  sumeq2  11366  summodc  11390  fsum3  11394  fsum2dlemstep  11441  ntrivcvgap0  11556  prodeq1f  11559  prodeq2w  11563  prodeq2  11564  prodmodc  11585  zproddc  11586  fprodseq  11590  fprodntrivap  11591  fprod2dlemstep  11629  ctinf  12430  ctiunct  12440  ssomct  12445  ptex  12712  bdsep2  14608  bdzfauscl  14612  strcoll2  14705  sscoll2  14710  subctctexmid  14720  nninfall  14728