Theorem exbidv 1813

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

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

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11ev  1816  2exbidv  1856  3exbidv  1857  eubidh  2020  eubid  2021  eleq1w  2226  eleq2w  2227  eleq1  2228  eleq2  2229  rexbidv2  2468  ceqsex2  2765  alexeq  2851  ceqex  2852  sbc5  2973  sbcex2  3003  sbcexg  3004  sbcabel  3031  eluni  3791  csbunig  3796  intab  3852  cbvopab1  4054  cbvopab1s  4056  axsep2  4100  zfauscl  4101  bnd2  4151  mss  4203  opeqex  4226  euotd  4231  snnex  4425  uniuni  4428  regexmid  4511  reg2exmid  4512  onintexmid  4549  reg3exmid  4556  nnregexmid  4597  opeliunxp  4658  csbxpg  4684  brcog  4770  elrn2g  4793  dfdmf  4796  csbdmg  4797  eldmg  4798  dfrnf  4844  elrn2  4845  elrnmpt1  4854  brcodir  4990  xp11m  5041  xpimasn  5051  csbrng  5064  elxp4  5090  elxp5  5091  dfco2a  5103  cores  5106  funimaexglem  5270  brprcneu  5478  ssimaexg  5547  dmfco  5553  fndmdif  5589  fmptco  5650  fliftf  5766  acexmidlem2  5838  acexmidlemv  5839  cbvoprab1  5910  cbvoprab2  5911  oprssdmm  6136  dmtpos  6220  tfrlemi1  6296  tfr1onlemaccex  6312  tfrcllemaccex  6325  ecdmn0m  6539  ereldm  6540  elqsn0m  6565  mapsn  6652  bren  6709  brdomg  6710  domeng  6714  ac6sfi  6860  ordiso  6997  ctssdclemr  7073  enumct  7076  ctssexmid  7110  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  acfun  7159  ccfunen  7201  cc1  7202  cc2lem  7203  cc2  7204  cc3  7205  recexnq  7327  prarloc  7440  genpdflem  7444  genpassl  7461  genpassu  7462  ltexprlemell  7535  ltexprlemelu  7536  ltexprlemm  7537  recexprlemell  7559  recexprlemelu  7560  cnm  7769  sup3exmid  8848  seq3f1olemp  10433  zfz1isolem1  10749  zfz1iso  10750  sumeq1  11292  sumeq2  11296  summodc  11320  fsum3  11324  fsum2dlemstep  11371  ntrivcvgap0  11486  prodeq1f  11489  prodeq2w  11493  prodeq2  11494  prodmodc  11515  zproddc  11516  fprodseq  11520  fprodntrivap  11521  fprod2dlemstep  11559  ctinf  12359  ctiunct  12369  ssomct  12374  bdsep2  13728  bdzfauscl  13732  strcoll2  13825  sscoll2  13830  subctctexmid  13841  nninfall  13849