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  3843  csbunig  3848  intab  3904  cbvopab1  4107  cbvopab1s  4109  axsep2  4153  zfauscl  4154  bnd2  4207  mss  4260  opeqex  4283  euotd  4288  snnex  4484  uniuni  4487  regexmid  4572  reg2exmid  4573  onintexmid  4610  reg3exmid  4617  nnregexmid  4658  opeliunxp  4719  csbxpg  4745  brcog  4834  elrn2g  4857  dfdmf  4860  csbdmg  4861  eldmg  4862  dfrnf  4908  elrn2  4909  elrnmpt1  4918  brcodir  5058  xp11m  5109  xpimasn  5119  csbrng  5132  elxp4  5158  elxp5  5159  dfco2a  5171  cores  5174  funimaexglem  5342  brprcneu  5554  ssimaexg  5626  dmfco  5632  fndmdif  5670  fmptco  5731  fliftf  5849  acexmidlem2  5922  acexmidlemv  5923  cbvoprab1  5998  cbvoprab2  5999  oprssdmm  6238  dmtpos  6323  tfrlemi1  6399  tfr1onlemaccex  6415  tfrcllemaccex  6428  ecdmn0m  6645  ereldm  6646  elqsn0m  6671  mapsn  6758  bren  6815  brdomg  6816  domeng  6820  ac6sfi  6968  ordiso  7111  ctssdclemr  7187  enumct  7190  ctssexmid  7225  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  acneq  7285  finacn  7287  acfun  7290  ccfunen  7347  cc1  7348  cc2lem  7349  cc2  7350  cc3  7351  acnccim  7355  recexnq  7474  prarloc  7587  genpdflem  7591  genpassl  7608  genpassu  7609  ltexprlemell  7682  ltexprlemelu  7683  ltexprlemm  7684  recexprlemell  7706  recexprlemelu  7707  cnm  7916  sup3exmid  9001  seq3f1olemp  10624  zfz1isolem1  10949  zfz1iso  10950  sumeq1  11537  sumeq2  11541  summodc  11565  fsum3  11569  fsum2dlemstep  11616  ntrivcvgap0  11731  prodeq1f  11734  prodeq2w  11738  prodeq2  11739  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodntrivap  11766  fprod2dlemstep  11804  ctinf  12672  ctiunct  12682  ssomct  12687  ptex  12966  igsumvalx  13091  gsumpropd  13094  gsumpropd2  13095  gsumress  13097  gsum0g  13098  islssm  13989  islssmg  13990  znleval  14285  bdsep2  15616  bdzfauscl  15620  strcoll2  15713  sscoll2  15718  subctctexmid  15731  domomsubct  15732  nninfall  15740