Theorem exbidv 1849

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1852  2exbidv  1892  3exbidv  1893  eubidh  2061  eubid  2062  eleq1w  2267  eleq2w  2268  eleq1  2269  eleq2  2270  rexbidv2  2510  ceqsex2  2815  alexeq  2903  ceqex  2904  sbc5  3026  sbcex2  3056  sbcexg  3057  sbcabel  3084  eluni  3862  csbunig  3867  intab  3923  cbvopab1  4128  cbvopab1s  4130  axsep2  4174  zfauscl  4175  bnd2  4228  mss  4283  opeqex  4307  euotd  4312  snnex  4508  uniuni  4511  regexmid  4596  reg2exmid  4597  onintexmid  4634  reg3exmid  4641  nnregexmid  4682  opeliunxp  4743  csbxpg  4769  brcog  4858  elrn2g  4881  dfdmf  4885  csbdmg  4886  eldmg  4887  dfrnf  4933  elrn2  4934  elrnmpt1  4943  brcodir  5084  xp11m  5135  xpimasn  5145  csbrng  5158  elxp4  5184  elxp5  5185  dfco2a  5197  cores  5200  funimaexglem  5371  brprcneu  5587  ssimaexg  5659  dmfco  5665  fndmdif  5703  fmptco  5764  fliftf  5886  acexmidlem2  5959  acexmidlemv  5960  cbvoprab1  6035  cbvoprab2  6036  oprssdmm  6275  dmtpos  6360  tfrlemi1  6436  tfr1onlemaccex  6452  tfrcllemaccex  6465  ecdmn0m  6682  ereldm  6683  elqsn0m  6708  mapsn  6795  breng  6852  bren  6853  brdom2g  6854  brdomg  6855  domeng  6859  en2  6931  ac6sfi  7016  ordiso  7159  ctssdclemr  7235  enumct  7238  ctssexmid  7273  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  acneq  7340  finacn  7342  acfun  7345  ccfunen  7406  cc1  7407  cc2lem  7408  cc2  7409  cc3  7410  acnccim  7414  recexnq  7533  prarloc  7646  genpdflem  7650  genpassl  7667  genpassu  7668  ltexprlemell  7741  ltexprlemelu  7742  ltexprlemm  7743  recexprlemell  7765  recexprlemelu  7766  cnm  7975  sup3exmid  9060  seq3f1olemp  10692  zfz1isolem1  11017  zfz1iso  11018  sumeq1  11751  sumeq2  11755  summodc  11779  fsum3  11783  fsum2dlemstep  11830  ntrivcvgap0  11945  prodeq1f  11948  prodeq2w  11952  prodeq2  11953  prodmodc  11974  zproddc  11975  fprodseq  11979  fprodntrivap  11980  fprod2dlemstep  12018  ctinf  12886  ctiunct  12896  ssomct  12901  ptex  13181  igsumvalx  13306  gsumpropd  13309  gsumpropd2  13310  gsumress  13312  gsum0g  13313  islssm  14204  islssmg  14205  znleval  14500  uhgrm  15759  lpvtx  15760  incistruhgr  15771  upgrex  15784  uhgredgm  15812  bdsep2  15991  bdzfauscl  15995  strcoll2  16088  sscoll2  16093  subctctexmid  16109  domomsubct  16110  nninfall  16118