Metamath Proof Explorer


Theorem sbhypf

Description: Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004) (Proof shortened by Wolf Lammen, 25-Jan-2025)

Ref Expression
Hypotheses sbhypf.1 𝑥 𝜓
sbhypf.2 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
Assertion sbhypf ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 sbhypf.1 𝑥 𝜓
2 sbhypf.2 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
3 2 sbimi ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 → [ 𝑦 / 𝑥 ] ( 𝜑𝜓 ) )
4 eqsb1 ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴𝑦 = 𝐴 )
5 1 sbf ( [ 𝑦 / 𝑥 ] 𝜓𝜓 )
6 5 sblbis ( [ 𝑦 / 𝑥 ] ( 𝜑𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑𝜓 ) )
7 3 4 6 3imtr3i ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑𝜓 ) )