Theorem exbidv 1878

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11ev  1881  2exbidv  1921  3exbidv  1922  eubidh  2092  eubid  2093  eleq1w  2299  eleq2w  2300  eleq1  2301  eleq2  2302  rexbidv2  2553  ceqsex2  2863  alexeq  2952  ceqex  2953  sbc5  3075  sbcex2  3105  sbcexg  3106  sbcabel  3134  eluni  3938  csbunig  3943  intab  3999  cbvopab1  4204  cbvopab1s  4206  axsepg  4250  sepg  4251  zfausclOLD  4253  bnd2  4310  mss  4366  opeqex  4390  euotd  4395  snnex  4594  uniuni  4597  regexmid  4682  reg2exmid  4683  onintexmid  4720  reg3exmid  4727  nnregexmid  4768  opeliunxp  4830  csbxpg  4856  brcog  4947  elrn2g  4970  dfdmf  4974  csbdmg  4975  eldmg  4976  dfrnf  5023  elrn2  5024  elrnmpt1  5033  brcodir  5175  xp11m  5226  xpimasn  5236  csbrng  5249  elxp4  5275  elxp5  5276  dfco2a  5288  cores  5291  funimaexglem  5464  brprcneu  5688  ssimaexg  5765  dmfco  5773  fndmdif  5814  fmptco  5874  fliftf  6005  acexmidlem2  6082  acexmidlemv  6083  cbvoprab1  6160  cbvoprab2  6161  oprssdmm  6405  dmtpos  6527  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  ecdmn0m  6851  ereldm  6852  elqsn0m  6877  mapsnd  6970  mapsn  6972  breng  7029  bren  7030  brdom2g  7031  brdomg  7032  domeng  7036  mapsnend  7099  en2  7112  ac6sfi  7202  ordiso  7376  ctssdclemr  7452  enumct  7455  ctssexmid  7490  sspw1or2  7544  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acneq  7558  finacn  7560  acfun  7563  ccfunen  7630  cc1  7631  cc2lem  7632  cc2  7633  cc3  7634  acnccim  7638  recexnq  7757  prarloc  7870  genpdflem  7874  genpassl  7891  genpassu  7892  ltexprlemell  7965  ltexprlemelu  7966  ltexprlemm  7967  recexprlemell  7989  recexprlemelu  7990  cnm  8199  sup3exmid  9287  seq3f1olemp  10952  zfz1isolem1  11292  zfz1iso  11293  sumeq1  12121  sumeq2  12125  summodc  12150  fsum3  12154  fsum2dlemstep  12201  ntrivcvgap0  12316  prodeq1f  12319  prodeq2w  12323  prodeq2  12324  prodmodc  12345  zproddc  12346  fprodseq  12350  fprodntrivap  12351  fprod2dlemstep  12389  ctinf  13321  ctiunct  13331  ssomct  13336  ptex  13618  gzsumvalx  13709  gzsumress  13712  gzsum0  13713  gsumvalfi  14152  islssm  14694  islssmg  14695  znleval  14988  uhgrm  16319  lpvtx  16320  incistruhgr  16331  upgrex  16344  uhgredgm  16377  subgruhgredgdm  16511  1loopgrvd2fi  16546  wlkm  16580  bdsep2  16912  bdsepg  16916  strcoll2  17009  sscoll2  17014  subctctexmid  17030  domomsubct  17031  wexmiddiffilem  17043  wexmiddifxylem  17045  nninfall  17052