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  2842  alexeq  2930  ceqex  2931  sbc5  3053  sbcex2  3083  sbcexg  3084  sbcabel  3112  eluni  3894  csbunig  3899  intab  3955  cbvopab1  4160  cbvopab1s  4162  axsep2  4206  zfauscl  4207  bnd2  4261  mss  4316  opeqex  4340  euotd  4345  snnex  4543  uniuni  4546  regexmid  4631  reg2exmid  4632  onintexmid  4669  reg3exmid  4676  nnregexmid  4717  opeliunxp  4779  csbxpg  4805  brcog  4895  elrn2g  4918  dfdmf  4922  csbdmg  4923  eldmg  4924  dfrnf  4971  elrn2  4972  elrnmpt1  4981  brcodir  5122  xp11m  5173  xpimasn  5183  csbrng  5196  elxp4  5222  elxp5  5223  dfco2a  5235  cores  5238  funimaexglem  5410  brprcneu  5628  ssimaexg  5704  dmfco  5710  fndmdif  5748  fmptco  5809  fliftf  5935  acexmidlem2  6010  acexmidlemv  6011  cbvoprab1  6088  cbvoprab2  6089  oprssdmm  6329  dmtpos  6417  tfrlemi1  6493  tfr1onlemaccex  6509  tfrcllemaccex  6522  ecdmn0m  6741  ereldm  6742  elqsn0m  6767  mapsn  6854  breng  6911  bren  6912  brdom2g  6913  brdomg  6914  domeng  6918  en2  6993  ac6sfi  7080  ordiso  7226  ctssdclemr  7302  enumct  7305  ctssexmid  7340  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  acneq  7407  finacn  7409  acfun  7412  ccfunen  7473  cc1  7474  cc2lem  7475  cc2  7476  cc3  7477  acnccim  7481  recexnq  7600  prarloc  7713  genpdflem  7717  genpassl  7734  genpassu  7735  ltexprlemell  7808  ltexprlemelu  7809  ltexprlemm  7810  recexprlemell  7832  recexprlemelu  7833  cnm  8042  sup3exmid  9127  seq3f1olemp  10767  zfz1isolem1  11094  zfz1iso  11095  sumeq1  11906  sumeq2  11910  summodc  11934  fsum3  11938  fsum2dlemstep  11985  ntrivcvgap0  12100  prodeq1f  12103  prodeq2w  12107  prodeq2  12108  prodmodc  12129  zproddc  12130  fprodseq  12134  fprodntrivap  12135  fprod2dlemstep  12173  ctinf  13041  ctiunct  13051  ssomct  13056  ptex  13337  igsumvalx  13462  gsumpropd  13465  gsumpropd2  13466  gsumress  13468  gsum0g  13469  islssm  14361  islssmg  14362  znleval  14657  uhgrm  15919  lpvtx  15920  incistruhgr  15931  upgrex  15944  uhgredgm  15975  1loopgrvd2fi  16111  wlkm  16136  bdsep2  16417  bdzfauscl  16421  strcoll2  16514  sscoll2  16519  subctctexmid  16537  domomsubct  16538  nninfall  16547