Metamath Proof Explorer


Theorem sb1

Description: One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition ( sb5 ) or a nonfreeness hypothesis ( sb5f ). Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sb1v when possible. (Contributed by NM, 13-May-1993) Revise df-sb . (Revised by Wolf Lammen, 21-Feb-2024) (New usage is discouraged.)

Ref Expression
Assertion sb1 ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) )

Proof

Step Hyp Ref Expression
1 spsbe ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 )
2 pm3.2 ( 𝑥 = 𝑦 → ( 𝜑 → ( 𝑥 = 𝑦𝜑 ) ) )
3 2 aleximi ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
4 1 3 syl5 ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
5 sb3b ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
6 5 biimpd ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
7 4 6 pm2.61i ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) )