Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Metamath formal systems
mrsubvr
Next ⟩
mrsubff
Metamath Proof Explorer
Ascii
Unicode
Theorem
mrsubvr
Description:
The value of a substituted variable.
(Contributed by
Mario Carneiro
, 18-Jul-2016)
Ref
Expression
Hypotheses
mrsubvr.v
⊢
V
=
mVR
⁡
T
mrsubvr.r
⊢
R
=
mREx
⁡
T
mrsubvr.s
⊢
S
=
mRSubst
⁡
T
Assertion
mrsubvr
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
A
→
S
⁡
F
⁡
〈“
X
”〉
=
F
⁡
X
Proof
Step
Hyp
Ref
Expression
1
mrsubvr.v
⊢
V
=
mVR
⁡
T
2
mrsubvr.r
⊢
R
=
mREx
⁡
T
3
mrsubvr.s
⊢
S
=
mRSubst
⁡
T
4
ssun2
⊢
V
⊆
mCN
⁡
T
∪
V
5
simp2
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
A
→
A
⊆
V
6
simp3
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
A
→
X
∈
A
7
5
6
sseldd
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
A
→
X
∈
V
8
4
7
sseldi
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
A
→
X
∈
mCN
⁡
T
∪
V
9
eqid
⊢
mCN
⁡
T
=
mCN
⁡
T
10
9
1
2
3
mrsubcv
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
mCN
⁡
T
∪
V
→
S
⁡
F
⁡
〈“
X
”〉
=
if
X
∈
A
F
⁡
X
〈“
X
”〉
11
8
10
syld3an3
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
A
→
S
⁡
F
⁡
〈“
X
”〉
=
if
X
∈
A
F
⁡
X
〈“
X
”〉
12
iftrue
⊢
X
∈
A
→
if
X
∈
A
F
⁡
X
〈“
X
”〉
=
F
⁡
X
13
12
3ad2ant3
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
A
→
if
X
∈
A
F
⁡
X
〈“
X
”〉
=
F
⁡
X
14
11
13
eqtrd
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
A
→
S
⁡
F
⁡
〈“
X
”〉
=
F
⁡
X