Metamath Proof Explorer

Theorem sbt

Description: A substitution into a theorem yields a theorem. See sbtALT for a shorter proof requiring more axioms. See chvar and chvarv for versions using implicit substitution. (Contributed by NM, 21-Jan-2004) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 20-Jul-2018) Revise df-sb . (Revised by Steven Nguyen, 6-Jul-2023) Revise df-sb again. (Revised by Wolf Lammen, 4-Feb-2026)

|- ph

|- [ t / x ] ph

 |-  ph

 |-  A. y ( y = t -> A. x ( x = y -> ph ) )

 |-  A. z ( z = t -> A. x ( x = z -> ph ) )

 |-  ( A. y ( y = t -> A. x ( x = y -> ph ) ) <-> A. z ( z = t -> A. x ( x = z -> ph ) ) )

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

 |-  [ t / x ] ph