Theorem exbidv 1871

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1874  2exbidv  1914  3exbidv  1915  eubidh  2083  eubid  2084  eleq1w  2290  eleq2w  2291  eleq1  2292  eleq2  2293  rexbidv2  2533  ceqsex2  2841  alexeq  2929  ceqex  2930  sbc5  3052  sbcex2  3082  sbcexg  3083  sbcabel  3111  eluni  3891  csbunig  3896  intab  3952  cbvopab1  4157  cbvopab1s  4159  axsep2  4203  zfauscl  4204  bnd2  4257  mss  4312  opeqex  4336  euotd  4341  snnex  4539  uniuni  4542  regexmid  4627  reg2exmid  4628  onintexmid  4665  reg3exmid  4672  nnregexmid  4713  opeliunxp  4774  csbxpg  4800  brcog  4889  elrn2g  4912  dfdmf  4916  csbdmg  4917  eldmg  4918  dfrnf  4965  elrn2  4966  elrnmpt1  4975  brcodir  5116  xp11m  5167  xpimasn  5177  csbrng  5190  elxp4  5216  elxp5  5217  dfco2a  5229  cores  5232  funimaexglem  5404  brprcneu  5622  ssimaexg  5698  dmfco  5704  fndmdif  5742  fmptco  5803  fliftf  5929  acexmidlem2  6004  acexmidlemv  6005  cbvoprab1  6082  cbvoprab2  6083  oprssdmm  6323  dmtpos  6408  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  ecdmn0m  6732  ereldm  6733  elqsn0m  6758  mapsn  6845  breng  6902  bren  6903  brdom2g  6904  brdomg  6905  domeng  6909  en2  6981  ac6sfi  7068  ordiso  7211  ctssdclemr  7287  enumct  7290  ctssexmid  7325  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  acneq  7392  finacn  7394  acfun  7397  ccfunen  7458  cc1  7459  cc2lem  7460  cc2  7461  cc3  7462  acnccim  7466  recexnq  7585  prarloc  7698  genpdflem  7702  genpassl  7719  genpassu  7720  ltexprlemell  7793  ltexprlemelu  7794  ltexprlemm  7795  recexprlemell  7817  recexprlemelu  7818  cnm  8027  sup3exmid  9112  seq3f1olemp  10745  zfz1isolem1  11070  zfz1iso  11071  sumeq1  11874  sumeq2  11878  summodc  11902  fsum3  11906  fsum2dlemstep  11953  ntrivcvgap0  12068  prodeq1f  12071  prodeq2w  12075  prodeq2  12076  prodmodc  12097  zproddc  12098  fprodseq  12102  fprodntrivap  12103  fprod2dlemstep  12141  ctinf  13009  ctiunct  13019  ssomct  13024  ptex  13305  igsumvalx  13430  gsumpropd  13433  gsumpropd2  13434  gsumress  13436  gsum0g  13437  islssm  14329  islssmg  14330  znleval  14625  uhgrm  15886  lpvtx  15887  incistruhgr  15898  upgrex  15911  uhgredgm  15942  wlkm  16060  bdsep2  16273  bdzfauscl  16277  strcoll2  16370  sscoll2  16375  subctctexmid  16395  domomsubct  16396  nninfall  16405