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  7283  exmidfodomrlemrALT  7284  acneq  7287  finacn  7289  acfun  7292  ccfunen  7349  cc1  7350  cc2lem  7351  cc2  7352  cc3  7353  acnccim  7357  recexnq  7476  prarloc  7589  genpdflem  7593  genpassl  7610  genpassu  7611  ltexprlemell  7684  ltexprlemelu  7685  ltexprlemm  7686  recexprlemell  7708  recexprlemelu  7709  cnm  7918  sup3exmid  9003  seq3f1olemp  10626  zfz1isolem1  10951  zfz1iso  10952  sumeq1  11539  sumeq2  11543  summodc  11567  fsum3  11571  fsum2dlemstep  11618  ntrivcvgap0  11733  prodeq1f  11736  prodeq2w  11740  prodeq2  11741  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodntrivap  11768  fprod2dlemstep  11806  ctinf  12674  ctiunct  12684  ssomct  12689  ptex  12968  igsumvalx  13093  gsumpropd  13096  gsumpropd2  13097  gsumress  13099  gsum0g  13100  islssm  13991  islssmg  13992  znleval  14287  bdsep2  15640  bdzfauscl  15644  strcoll2  15737  sscoll2  15742  subctctexmid  15755  domomsubct  15756  nninfall  15764