Metamath Proof Explorer

Theorem gm-sbtru

Description: Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019)

Ref Expression
Hypothesis gm-sbtru.1 
|- A e. _V
Assertion gm-sbtru 
|- ( [. A / x ]. T. <-> T. )

Proof

Step Hyp Ref Expression
1 gm-sbtru.1 
 |-  A e. _V
2 sbcg 
 |-  ( A e. _V -> ( [. A / x ]. T. <-> T. ) )
3 1 2 ax-mp 
 |-  ( [. A / x ]. T. <-> T. )