Theorem exbidv 1836

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1839  2exbidv  1879  3exbidv  1880  eubidh  2048  eubid  2049  eleq1w  2254  eleq2w  2255  eleq1  2256  eleq2  2257  rexbidv2  2497  ceqsex2  2800  alexeq  2886  ceqex  2887  sbc5  3009  sbcex2  3039  sbcexg  3040  sbcabel  3067  eluni  3838  csbunig  3843  intab  3899  cbvopab1  4102  cbvopab1s  4104  axsep2  4148  zfauscl  4149  bnd2  4202  mss  4255  opeqex  4278  euotd  4283  snnex  4479  uniuni  4482  regexmid  4567  reg2exmid  4568  onintexmid  4605  reg3exmid  4612  nnregexmid  4653  opeliunxp  4714  csbxpg  4740  brcog  4829  elrn2g  4852  dfdmf  4855  csbdmg  4856  eldmg  4857  dfrnf  4903  elrn2  4904  elrnmpt1  4913  brcodir  5053  xp11m  5104  xpimasn  5114  csbrng  5127  elxp4  5153  elxp5  5154  dfco2a  5166  cores  5169  funimaexglem  5337  brprcneu  5547  ssimaexg  5619  dmfco  5625  fndmdif  5663  fmptco  5724  fliftf  5842  acexmidlem2  5915  acexmidlemv  5916  cbvoprab1  5990  cbvoprab2  5991  oprssdmm  6224  dmtpos  6309  tfrlemi1  6385  tfr1onlemaccex  6401  tfrcllemaccex  6414  ecdmn0m  6631  ereldm  6632  elqsn0m  6657  mapsn  6744  bren  6801  brdomg  6802  domeng  6806  ac6sfi  6954  ordiso  7095  ctssdclemr  7171  enumct  7174  ctssexmid  7209  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  acfun  7267  ccfunen  7324  cc1  7325  cc2lem  7326  cc2  7327  cc3  7328  recexnq  7450  prarloc  7563  genpdflem  7567  genpassl  7584  genpassu  7585  ltexprlemell  7658  ltexprlemelu  7659  ltexprlemm  7660  recexprlemell  7682  recexprlemelu  7683  cnm  7892  sup3exmid  8976  seq3f1olemp  10586  zfz1isolem1  10911  zfz1iso  10912  sumeq1  11498  sumeq2  11502  summodc  11526  fsum3  11530  fsum2dlemstep  11577  ntrivcvgap0  11692  prodeq1f  11695  prodeq2w  11699  prodeq2  11700  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodntrivap  11727  fprod2dlemstep  11765  ctinf  12587  ctiunct  12597  ssomct  12602  ptex  12875  igsumvalx  12972  gsumpropd  12975  gsumpropd2  12976  gsumress  12978  gsum0g  12979  islssm  13853  islssmg  13854  znleval  14141  bdsep2  15378  bdzfauscl  15382  strcoll2  15475  sscoll2  15480  subctctexmid  15491  nninfall  15499