This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfsb

Description: Simplify definition df-sb by removing its provable hypothesis. (Contributed by Wolf Lammen, 5-Feb-2026)

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

Proof

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