Metamath Proof Explorer

Theorem dfsbimp

Description: A simple consequence of df-sb . (Contributed by Wolf Lammen, 4-Jun-2026)

Ref Expression
Assertion dfsbimp 
|- ( [ t / x ] ph -> A. y ( y = t -> A. x ( x = y -> ph ) ) )

Proof

Step Hyp Ref Expression
1 df-sb 
 |-  ( [ t / x ] ph <-> ( A. y ( y = t -> A. x ( x = y -> ph ) ) /\ A. z ( z = t -> A. x ( x = z -> ph ) ) ) )
2 1 simplbi 
 |-  ( [ t / x ] ph -> A. y ( y = t -> A. x ( x = y -> ph ) ) )