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  2779  alexeq  2865  ceqex  2866  sbc5  2988  sbcex2  3018  sbcexg  3019  sbcabel  3046  eluni  3814  csbunig  3819  intab  3875  cbvopab1  4078  cbvopab1s  4080  axsep2  4124  zfauscl  4125  bnd2  4175  mss  4228  opeqex  4251  euotd  4256  snnex  4450  uniuni  4453  regexmid  4536  reg2exmid  4537  onintexmid  4574  reg3exmid  4581  nnregexmid  4622  opeliunxp  4683  csbxpg  4709  brcog  4796  elrn2g  4819  dfdmf  4822  csbdmg  4823  eldmg  4824  dfrnf  4870  elrn2  4871  elrnmpt1  4880  brcodir  5018  xp11m  5069  xpimasn  5079  csbrng  5092  elxp4  5118  elxp5  5119  dfco2a  5131  cores  5134  funimaexglem  5301  brprcneu  5510  ssimaexg  5580  dmfco  5586  fndmdif  5623  fmptco  5684  fliftf  5802  acexmidlem2  5874  acexmidlemv  5875  cbvoprab1  5949  cbvoprab2  5950  oprssdmm  6174  dmtpos  6259  tfrlemi1  6335  tfr1onlemaccex  6351  tfrcllemaccex  6364  ecdmn0m  6579  ereldm  6580  elqsn0m  6605  mapsn  6692  bren  6749  brdomg  6750  domeng  6754  ac6sfi  6900  ordiso  7037  ctssdclemr  7113  enumct  7116  ctssexmid  7150  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  acfun  7208  ccfunen  7265  cc1  7266  cc2lem  7267  cc2  7268  cc3  7269  recexnq  7391  prarloc  7504  genpdflem  7508  genpassl  7525  genpassu  7526  ltexprlemell  7599  ltexprlemelu  7600  ltexprlemm  7601  recexprlemell  7623  recexprlemelu  7624  cnm  7833  sup3exmid  8916  seq3f1olemp  10504  zfz1isolem1  10822  zfz1iso  10823  sumeq1  11365  sumeq2  11369  summodc  11393  fsum3  11397  fsum2dlemstep  11444  ntrivcvgap0  11559  prodeq1f  11562  prodeq2w  11566  prodeq2  11567  prodmodc  11588  zproddc  11589  fprodseq  11593  fprodntrivap  11594  fprod2dlemstep  11632  ctinf  12433  ctiunct  12443  ssomct  12448  ptex  12718  islssm  13450  bdsep2  14723  bdzfauscl  14727  strcoll2  14820  sscoll2  14825  subctctexmid  14835  nninfall  14843