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  7377  ctssdclemr  7453  enumct  7456  ctssexmid  7491  sspw1or2  7545  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  acneq  7559  finacn  7561  acfun  7564  ccfunen  7631  cc1  7632  cc2lem  7633  cc2  7634  cc3  7635  acnccim  7639  recexnq  7758  prarloc  7871  genpdflem  7875  genpassl  7892  genpassu  7893  ltexprlemell  7966  ltexprlemelu  7967  ltexprlemm  7968  recexprlemell  7990  recexprlemelu  7991  cnm  8200  sup3exmid  9290  seq3f1olemp  10967  zfz1isolem1  11308  zfz1iso  11309  sumeq1  12140  sumeq2  12144  summodc  12169  fsum3  12173  fsum2dlemstep  12220  ntrivcvgap0  12335  prodeq1f  12338  prodeq2w  12342  prodeq2  12343  prodmodc  12364  zproddc  12365  fprodseq  12369  fprodntrivap  12370  fprod2dlemstep  12408  ctinf  13373  ctiunct  13383  ssomct  13388  ptex  13671  gzsumvalx  13762  gzsumress  13765  gzsum0  13766  gsumvalfi  14236  islssm  14778  islssmg  14779  znleval  15072  uhgrm  16485  lpvtx  16486  incistruhgr  16497  upgrex  16510  uhgredgm  16543  subgruhgredgdm  16677  1loopgrvd2fi  16712  wlkm  16746  bdsep2  17078  bdsepg  17082  strcoll2  17175  sscoll2  17180  subctctexmid  17196  domomsubct  17197  wexmiddiffilem  17209  wexmiddifxylem  17211  nninfall  17218