Metamath Proof Explorer


Theorem bj-ssbid1

Description: A special case of sbequ1 . (Contributed by BJ, 22-Dec-2020)

Ref Expression
Assertion bj-ssbid1 ( 𝜑 → [ 𝑥 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 equid 𝑥 = 𝑥
2 sbequ1 ( 𝑥 = 𝑥 → ( 𝜑 → [ 𝑥 / 𝑥 ] 𝜑 ) )
3 1 2 ax-mp ( 𝜑 → [ 𝑥 / 𝑥 ] 𝜑 )