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 𝐴 ∈ V
Assertion gm-sbtru ( [ 𝐴 / 𝑥 ] ⊤ ↔ ⊤ )

Proof

Step Hyp Ref Expression
1 gm-sbtru.1 𝐴 ∈ V
2 sbcg ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ⊤ ↔ ⊤ ) )
3 1 2 ax-mp ( [ 𝐴 / 𝑥 ] ⊤ ↔ ⊤ )