Theorem exbidv 1797

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

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

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11ev  1800  2exbidv  1840  3exbidv  1841  eubidh  2005  eubid  2006  eleq1w  2200  eleq2w  2201  eleq1  2202  eleq2  2203  rexbidv2  2440  ceqsex2  2726  alexeq  2811  ceqex  2812  sbc5  2932  sbcex2  2962  sbcexg  2963  sbcabel  2990  eluni  3739  csbunig  3744  intab  3800  cbvopab1  4001  cbvopab1s  4003  axsep2  4047  zfauscl  4048  bnd2  4097  mss  4148  opeqex  4171  euotd  4176  snnex  4369  uniuni  4372  regexmid  4450  reg2exmid  4451  onintexmid  4487  reg3exmid  4494  nnregexmid  4534  opeliunxp  4594  csbxpg  4620  brcog  4706  elrn2g  4729  dfdmf  4732  csbdmg  4733  eldmg  4734  dfrnf  4780  elrn2  4781  elrnmpt1  4790  brcodir  4926  xp11m  4977  xpimasn  4987  csbrng  5000  elxp4  5026  elxp5  5027  dfco2a  5039  cores  5042  funimaexglem  5206  brprcneu  5414  ssimaexg  5483  dmfco  5489  fndmdif  5525  fmptco  5586  fliftf  5700  acexmidlem2  5771  acexmidlemv  5772  cbvoprab1  5843  cbvoprab2  5844  oprssdmm  6069  dmtpos  6153  tfrlemi1  6229  tfr1onlemaccex  6245  tfrcllemaccex  6258  ecdmn0m  6471  ereldm  6472  elqsn0m  6497  mapsn  6584  bren  6641  brdomg  6642  domeng  6646  ac6sfi  6792  ordiso  6921  ctssdclemr  6997  enumct  7000  ctssexmid  7024  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  acfun  7063  ccfunen  7079  recexnq  7198  prarloc  7311  genpdflem  7315  genpassl  7332  genpassu  7333  ltexprlemell  7406  ltexprlemelu  7407  ltexprlemm  7408  recexprlemell  7430  recexprlemelu  7431  cnm  7640  sup3exmid  8715  seq3f1olemp  10275  zfz1isolem1  10583  zfz1iso  10584  sumeq1  11124  sumeq2  11128  summodc  11152  fsum3  11156  fsum2dlemstep  11203  ntrivcvgap0  11318  prodeq1f  11321  prodeq2w  11325  prodeq2  11326  prodmodc  11347  ctinf  11943  ctiunct  11953  bdsep2  13084  bdzfauscl  13088  strcoll2  13181  subctctexmid  13196  nninfall  13204