Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Giovanni Mascellani
Tools for automatic proof building
gm-sbtru
Next ⟩
sbfal
Metamath Proof Explorer
Ascii
Unicode
Theorem
gm-sbtru
Description:
Substitution does not change truth.
(Contributed by
Giovanni Mascellani
, 24-May-2019)
Ref
Expression
Hypothesis
gm-sbtru.1
⊢
A
∈
V
Assertion
gm-sbtru
⊢
[
˙
A
/
x
]
˙
⊤
↔
⊤
Proof
Step
Hyp
Ref
Expression
1
gm-sbtru.1
⊢
A
∈
V
2
sbcg
⊢
A
∈
V
→
[
˙
A
/
x
]
˙
⊤
↔
⊤
3
1
2
ax-mp
⊢
[
˙
A
/
x
]
˙
⊤
↔
⊤