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  7214  ctssdclemr  7290  enumct  7293  ctssexmid  7328  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acneq  7395  finacn  7397  acfun  7400  ccfunen  7461  cc1  7462  cc2lem  7463  cc2  7464  cc3  7465  acnccim  7469  recexnq  7588  prarloc  7701  genpdflem  7705  genpassl  7722  genpassu  7723  ltexprlemell  7796  ltexprlemelu  7797  ltexprlemm  7798  recexprlemell  7820  recexprlemelu  7821  cnm  8030  sup3exmid  9115  seq3f1olemp  10749  zfz1isolem1  11075  zfz1iso  11076  sumeq1  11881  sumeq2  11885  summodc  11909  fsum3  11913  fsum2dlemstep  11960  ntrivcvgap0  12075  prodeq1f  12078  prodeq2w  12082  prodeq2  12083  prodmodc  12104  zproddc  12105  fprodseq  12109  fprodntrivap  12110  fprod2dlemstep  12148  ctinf  13016  ctiunct  13026  ssomct  13031  ptex  13312  igsumvalx  13437  gsumpropd  13440  gsumpropd2  13441  gsumress  13443  gsum0g  13444  islssm  14336  islssmg  14337  znleval  14632  uhgrm  15893  lpvtx  15894  incistruhgr  15905  upgrex  15918  uhgredgm  15949  wlkm  16080  bdsep2  16304  bdzfauscl  16308  strcoll2  16401  sscoll2  16406  subctctexmid  16425  domomsubct  16426  nninfall  16435