Theorem sb2v 2302

Description: Version of sb2 2481 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by BJ, 31-May-2019.)

Assertion

Ref	Expression
sb2v	⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem sb2v

Step	Hyp	Ref	Expression
1		sp 2226	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜑))
2		equs4v 2109	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
3		df-sb 2070	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
4	1, 2, 3	sylanbrc 580	1 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)

Syntax hints:   → wi 4   ∧ wa 386  ∀wal 1656  ∃wex 1880  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-12 2222

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-sb 2070

This theorem is referenced by:  stdpc4v  2303  equsb1v  2306  sb6  2309  sbi1v  2337  iota4  6103  bj-sb3v  33286  bj-hbs1  33287  bj-hbsb2av  33289  wl-lem-moexsb  33893  absnsb  41962