Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Metamath formal systems
msubrsub
Next ⟩
msubty
Metamath Proof Explorer
Ascii
Unicode
Theorem
msubrsub
Description:
A substitution applied to an expression.
(Contributed by
Mario Carneiro
, 18-Jul-2016)
Ref
Expression
Hypotheses
msubffval.v
⊢
V
=
mVR
⁡
T
msubffval.r
⊢
R
=
mREx
⁡
T
msubffval.s
⊢
S
=
mSubst
⁡
T
msubffval.e
⊢
E
=
mEx
⁡
T
msubffval.o
⊢
O
=
mRSubst
⁡
T
Assertion
msubrsub
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
E
→
2
nd
⁡
S
⁡
F
⁡
X
=
O
⁡
F
⁡
2
nd
⁡
X
Proof
Step
Hyp
Ref
Expression
1
msubffval.v
⊢
V
=
mVR
⁡
T
2
msubffval.r
⊢
R
=
mREx
⁡
T
3
msubffval.s
⊢
S
=
mSubst
⁡
T
4
msubffval.e
⊢
E
=
mEx
⁡
T
5
msubffval.o
⊢
O
=
mRSubst
⁡
T
6
1
2
3
4
5
msubval
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
E
→
S
⁡
F
⁡
X
=
1
st
⁡
X
O
⁡
F
⁡
2
nd
⁡
X
7
fvex
⊢
1
st
⁡
X
∈
V
8
fvex
⊢
O
⁡
F
⁡
2
nd
⁡
X
∈
V
9
7
8
op2ndd
⊢
S
⁡
F
⁡
X
=
1
st
⁡
X
O
⁡
F
⁡
2
nd
⁡
X
→
2
nd
⁡
S
⁡
F
⁡
X
=
O
⁡
F
⁡
2
nd
⁡
X
10
6
9
syl
⊢
F
:
A
⟶
R
∧
A
⊆
V
∧
X
∈
E
→
2
nd
⁡
S
⁡
F
⁡
X
=
O
⁡
F
⁡
2
nd
⁡
X