Theorem exbidv 1873

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1876  2exbidv  1916  3exbidv  1917  eubidh  2085  eubid  2086  eleq1w  2292  eleq2w  2293  eleq1  2294  eleq2  2295  rexbidv2  2536  ceqsex2  2845  alexeq  2933  ceqex  2934  sbc5  3056  sbcex2  3086  sbcexg  3087  sbcabel  3115  eluni  3901  csbunig  3906  intab  3962  cbvopab1  4167  cbvopab1s  4169  axsep2  4213  zfauscl  4214  bnd2  4269  mss  4324  opeqex  4348  euotd  4353  snnex  4551  uniuni  4554  regexmid  4639  reg2exmid  4640  onintexmid  4677  reg3exmid  4684  nnregexmid  4725  opeliunxp  4787  csbxpg  4813  brcog  4903  elrn2g  4926  dfdmf  4930  csbdmg  4931  eldmg  4932  dfrnf  4979  elrn2  4980  elrnmpt1  4989  brcodir  5131  xp11m  5182  xpimasn  5192  csbrng  5205  elxp4  5231  elxp5  5232  dfco2a  5244  cores  5247  funimaexglem  5420  brprcneu  5641  ssimaexg  5717  dmfco  5723  fndmdif  5761  fmptco  5821  fliftf  5950  acexmidlem2  6025  acexmidlemv  6026  cbvoprab1  6103  cbvoprab2  6104  oprssdmm  6343  dmtpos  6465  tfrlemi1  6541  tfr1onlemaccex  6557  tfrcllemaccex  6570  ecdmn0m  6789  ereldm  6790  elqsn0m  6815  mapsn  6902  breng  6959  bren  6960  brdom2g  6961  brdomg  6962  domeng  6966  en2  7041  ac6sfi  7130  ordiso  7278  ctssdclemr  7354  enumct  7357  ctssexmid  7392  sspw1or2  7446  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  acneq  7460  finacn  7462  acfun  7465  ccfunen  7526  cc1  7527  cc2lem  7528  cc2  7529  cc3  7530  acnccim  7534  recexnq  7653  prarloc  7766  genpdflem  7770  genpassl  7787  genpassu  7788  ltexprlemell  7861  ltexprlemelu  7862  ltexprlemm  7863  recexprlemell  7885  recexprlemelu  7886  cnm  8095  sup3exmid  9179  seq3f1olemp  10823  zfz1isolem1  11150  zfz1iso  11151  sumeq1  11978  sumeq2  11982  summodc  12007  fsum3  12011  fsum2dlemstep  12058  ntrivcvgap0  12173  prodeq1f  12176  prodeq2w  12180  prodeq2  12181  prodmodc  12202  zproddc  12203  fprodseq  12207  fprodntrivap  12208  fprod2dlemstep  12246  ctinf  13114  ctiunct  13124  ssomct  13129  ptex  13410  igsumvalx  13535  gsumpropd  13538  gsumpropd2  13539  gsumress  13541  gsum0g  13542  islssm  14436  islssmg  14437  znleval  14732  uhgrm  16002  lpvtx  16003  incistruhgr  16014  upgrex  16027  uhgredgm  16060  subgruhgredgdm  16194  1loopgrvd2fi  16229  wlkm  16263  bdsep2  16585  bdzfauscl  16589  strcoll2  16682  sscoll2  16687  subctctexmid  16705  domomsubct  16706  nninfall  16718  gfsumval  16792