Theorem exbidv 1839

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1842  2exbidv  1882  3exbidv  1883  eubidh  2051  eubid  2052  eleq1w  2257  eleq2w  2258  eleq1  2259  eleq2  2260  rexbidv2  2500  ceqsex2  2804  alexeq  2890  ceqex  2891  sbc5  3013  sbcex2  3043  sbcexg  3044  sbcabel  3071  eluni  3842  csbunig  3847  intab  3903  cbvopab1  4106  cbvopab1s  4108  axsep2  4152  zfauscl  4153  bnd2  4206  mss  4259  opeqex  4282  euotd  4287  snnex  4483  uniuni  4486  regexmid  4571  reg2exmid  4572  onintexmid  4609  reg3exmid  4616  nnregexmid  4657  opeliunxp  4718  csbxpg  4744  brcog  4833  elrn2g  4856  dfdmf  4859  csbdmg  4860  eldmg  4861  dfrnf  4907  elrn2  4908  elrnmpt1  4917  brcodir  5057  xp11m  5108  xpimasn  5118  csbrng  5131  elxp4  5157  elxp5  5158  dfco2a  5170  cores  5173  funimaexglem  5341  brprcneu  5551  ssimaexg  5623  dmfco  5629  fndmdif  5667  fmptco  5728  fliftf  5846  acexmidlem2  5919  acexmidlemv  5920  cbvoprab1  5994  cbvoprab2  5995  oprssdmm  6229  dmtpos  6314  tfrlemi1  6390  tfr1onlemaccex  6406  tfrcllemaccex  6419  ecdmn0m  6636  ereldm  6637  elqsn0m  6662  mapsn  6749  bren  6806  brdomg  6807  domeng  6811  ac6sfi  6959  ordiso  7102  ctssdclemr  7178  enumct  7181  ctssexmid  7216  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  acfun  7274  ccfunen  7331  cc1  7332  cc2lem  7333  cc2  7334  cc3  7335  recexnq  7457  prarloc  7570  genpdflem  7574  genpassl  7591  genpassu  7592  ltexprlemell  7665  ltexprlemelu  7666  ltexprlemm  7667  recexprlemell  7689  recexprlemelu  7690  cnm  7899  sup3exmid  8984  seq3f1olemp  10607  zfz1isolem1  10932  zfz1iso  10933  sumeq1  11520  sumeq2  11524  summodc  11548  fsum3  11552  fsum2dlemstep  11599  ntrivcvgap0  11714  prodeq1f  11717  prodeq2w  11721  prodeq2  11722  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodntrivap  11749  fprod2dlemstep  11787  ctinf  12647  ctiunct  12657  ssomct  12662  ptex  12935  igsumvalx  13032  gsumpropd  13035  gsumpropd2  13036  gsumress  13038  gsum0g  13039  islssm  13913  islssmg  13914  znleval  14209  bdsep2  15532  bdzfauscl  15536  strcoll2  15629  sscoll2  15634  subctctexmid  15645  nninfall  15653