Theorem exbidv 1847

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

Syntax hints:   → wi 4   ↔ wb 105  ∃wex 1514

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1850  2exbidv  1890  3exbidv  1891  eubidh  2059  eubid  2060  eleq1w  2265  eleq2w  2266  eleq1  2267  eleq2  2268  rexbidv2  2508  ceqsex2  2812  alexeq  2898  ceqex  2899  sbc5  3021  sbcex2  3051  sbcexg  3052  sbcabel  3079  eluni  3852  csbunig  3857  intab  3913  cbvopab1  4116  cbvopab1s  4118  axsep2  4162  zfauscl  4163  bnd2  4216  mss  4269  opeqex  4293  euotd  4298  snnex  4494  uniuni  4497  regexmid  4582  reg2exmid  4583  onintexmid  4620  reg3exmid  4627  nnregexmid  4668  opeliunxp  4729  csbxpg  4755  brcog  4844  elrn2g  4867  dfdmf  4870  csbdmg  4871  eldmg  4872  dfrnf  4918  elrn2  4919  elrnmpt1  4928  brcodir  5069  xp11m  5120  xpimasn  5130  csbrng  5143  elxp4  5169  elxp5  5170  dfco2a  5182  cores  5185  funimaexglem  5356  brprcneu  5568  ssimaexg  5640  dmfco  5646  fndmdif  5684  fmptco  5745  fliftf  5867  acexmidlem2  5940  acexmidlemv  5941  cbvoprab1  6016  cbvoprab2  6017  oprssdmm  6256  dmtpos  6341  tfrlemi1  6417  tfr1onlemaccex  6433  tfrcllemaccex  6446  ecdmn0m  6663  ereldm  6664  elqsn0m  6689  mapsn  6776  breng  6833  bren  6834  brdom2g  6835  brdomg  6836  domeng  6840  en2  6911  ac6sfi  6994  ordiso  7137  ctssdclemr  7213  enumct  7216  ctssexmid  7251  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  acneq  7313  finacn  7315  acfun  7318  ccfunen  7375  cc1  7376  cc2lem  7377  cc2  7378  cc3  7379  acnccim  7383  recexnq  7502  prarloc  7615  genpdflem  7619  genpassl  7636  genpassu  7637  ltexprlemell  7710  ltexprlemelu  7711  ltexprlemm  7712  recexprlemell  7734  recexprlemelu  7735  cnm  7944  sup3exmid  9029  seq3f1olemp  10658  zfz1isolem1  10983  zfz1iso  10984  sumeq1  11637  sumeq2  11641  summodc  11665  fsum3  11669  fsum2dlemstep  11716  ntrivcvgap0  11831  prodeq1f  11834  prodeq2w  11838  prodeq2  11839  prodmodc  11860  zproddc  11861  fprodseq  11865  fprodntrivap  11866  fprod2dlemstep  11904  ctinf  12772  ctiunct  12782  ssomct  12787  ptex  13067  igsumvalx  13192  gsumpropd  13195  gsumpropd2  13196  gsumress  13198  gsum0g  13199  islssm  14090  islssmg  14091  znleval  14386  bdsep2  15784  bdzfauscl  15788  strcoll2  15881  sscoll2  15886  subctctexmid  15899  domomsubct  15900  nninfall  15908