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  3890  csbunig  3895  intab  3951  cbvopab1  4156  cbvopab1s  4158  axsep2  4202  zfauscl  4203  bnd2  4256  mss  4311  opeqex  4335  euotd  4340  snnex  4538  uniuni  4541  regexmid  4626  reg2exmid  4627  onintexmid  4664  reg3exmid  4671  nnregexmid  4712  opeliunxp  4773  csbxpg  4799  brcog  4888  elrn2g  4911  dfdmf  4915  csbdmg  4916  eldmg  4917  dfrnf  4964  elrn2  4965  elrnmpt1  4974  brcodir  5115  xp11m  5166  xpimasn  5176  csbrng  5189  elxp4  5215  elxp5  5216  dfco2a  5228  cores  5231  funimaexglem  5403  brprcneu  5619  ssimaexg  5695  dmfco  5701  fndmdif  5739  fmptco  5800  fliftf  5922  acexmidlem2  5997  acexmidlemv  5998  cbvoprab1  6075  cbvoprab2  6076  oprssdmm  6315  dmtpos  6400  tfrlemi1  6476  tfr1onlemaccex  6492  tfrcllemaccex  6505  ecdmn0m  6722  ereldm  6723  elqsn0m  6748  mapsn  6835  breng  6892  bren  6893  brdom2g  6894  brdomg  6895  domeng  6899  en2  6971  ac6sfi  7056  ordiso  7199  ctssdclemr  7275  enumct  7278  ctssexmid  7313  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  acneq  7380  finacn  7382  acfun  7385  ccfunen  7446  cc1  7447  cc2lem  7448  cc2  7449  cc3  7450  acnccim  7454  recexnq  7573  prarloc  7686  genpdflem  7690  genpassl  7707  genpassu  7708  ltexprlemell  7781  ltexprlemelu  7782  ltexprlemm  7783  recexprlemell  7805  recexprlemelu  7806  cnm  8015  sup3exmid  9100  seq3f1olemp  10732  zfz1isolem1  11057  zfz1iso  11058  sumeq1  11861  sumeq2  11865  summodc  11889  fsum3  11893  fsum2dlemstep  11940  ntrivcvgap0  12055  prodeq1f  12058  prodeq2w  12062  prodeq2  12063  prodmodc  12084  zproddc  12085  fprodseq  12089  fprodntrivap  12090  fprod2dlemstep  12128  ctinf  12996  ctiunct  13006  ssomct  13011  ptex  13292  igsumvalx  13417  gsumpropd  13420  gsumpropd2  13421  gsumress  13423  gsum0g  13424  islssm  14315  islssmg  14316  znleval  14611  uhgrm  15872  lpvtx  15873  incistruhgr  15884  upgrex  15897  uhgredgm  15928  wlkm  16038  bdsep2  16207  bdzfauscl  16211  strcoll2  16304  sscoll2  16309  subctctexmid  16325  domomsubct  16326  nninfall  16334