Metamath Proof Explorer


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 sselid 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