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  9289  seq3f1olemp  10965  zfz1isolem1  11306  zfz1iso  11307  sumeq1  12137  sumeq2  12141  summodc  12166  fsum3  12170  fsum2dlemstep  12217  ntrivcvgap0  12332  prodeq1f  12335  prodeq2w  12339  prodeq2  12340  prodmodc  12361  zproddc  12362  fprodseq  12366  fprodntrivap  12367  fprod2dlemstep  12405  ctinf  13370  ctiunct  13380  ssomct  13385  ptex  13667  gzsumvalx  13758  gzsumress  13761  gzsum0  13762  gsumvalfi  14201  islssm  14743  islssmg  14744  znleval  15037  uhgrm  16417  lpvtx  16418  incistruhgr  16429  upgrex  16442  uhgredgm  16475  subgruhgredgdm  16609  1loopgrvd2fi  16644  wlkm  16678  bdsep2  17010  bdsepg  17014  strcoll2  17107  sscoll2  17112  subctctexmid  17128  domomsubct  17129  wexmiddiffilem  17141  wexmiddifxylem  17143  nninfall  17150