Theorem sb4a 2385

Description: A version of sb4 2384 that doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)

Assertion

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

Proof of Theorem sb4a

Step	Hyp	Ref	Expression
1		sb1 1940	. 2 ⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑))
2		equs5a 2376	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
3	1, 2	syl 17	1 ⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))

Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1521  ∃wex 1744  [wsb 1937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087  ax-13 2282

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-sb 1938

This theorem is referenced by:  hbsb2a  2389  sb6f  2413  bj-hbsb2av  32885