Theorem exbidv 1747

Description: Formula-building rule for existential quantifier (deduction rule). (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 1460	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1546	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 103  ∃wex 1422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ax11ev  1750  2exbidv  1790  3exbidv  1791  eubidh  1948  eubid  1949  eleq1  2142  eleq2  2143  rexbidv2  2372  ceqsex2  2640  alexeq  2722  ceqex  2723  sbc5  2839  sbcex2  2868  sbcexg  2869  sbcabel  2896  eluni  3612  csbunig  3617  intab  3673  cbvopab1  3859  cbvopab1s  3861  axsep2  3905  zfauscl  3906  bnd2  3955  mss  3989  opeqex  4012  euotd  4017  snnex  4207  uniuni  4209  regexmid  4286  reg2exmid  4287  onintexmid  4323  reg3exmid  4330  nnregexmid  4368  opeliunxp  4421  csbxpg  4447  brcog  4530  elrn2g  4553  dfdmf  4556  csbdmg  4557  eldmg  4558  dfrnf  4603  elrn2  4604  elrnmpt1  4613  brcodir  4742  xp11m  4789  xpimasn  4799  csbrng  4812  elxp4  4838  elxp5  4839  dfco2a  4851  cores  4854  funimaexglem  5013  brprcneu  5202  ssimaexg  5267  dmfco  5273  fndmdif  5304  fmptco  5362  fliftf  5470  acexmidlem2  5540  acexmidlemv  5541  cbvoprab1  5607  cbvoprab2  5608  dmtpos  5905  tfrlemi1  5981  tfr1onlemaccex  5997  tfrcllemaccex  6010  ecdmn0m  6214  ereldm  6215  elqsn0m  6240  bren  6294  brdomg  6295  domeng  6299  ac6sfi  6431  ordiso  6506  recexnq  6642  prarloc  6755  genpdflem  6759  genpassl  6776  genpassu  6777  ltexprlemell  6850  ltexprlemelu  6851  ltexprlemm  6852  recexprlemell  6874  recexprlemelu  6875  sumeq1  10330  sumeq2d  10334  sumeq2  10335  bdsep2  10835  bdzfauscl  10839  strcoll2  10936