Theorem mrsubvr

Description: The value of a substituted variable. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubvr.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mrsubvr.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	mrsubvr.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion	mrsubvr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ ⟨“ 𝑋 ”⟩ ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		mrsubvr.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mrsubvr.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		mrsubvr.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
4		ssun2	⊢ 𝑉 ⊆ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 )
5		simp2	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝐴 ⊆ 𝑉 )
6		simp3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
7	5 6	sseldd	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝑉 )
8	4 7	sseldi	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
9		eqid	⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
10	9 1 2 3	mrsubcv	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) → ( ( 𝑆 ‘ 𝐹 ) ‘ ⟨“ 𝑋 ”⟩ ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
11	8 10	syld3an3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ ⟨“ 𝑋 ”⟩ ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
12		iftrue	⊢ ( 𝑋 ∈ 𝐴 → if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) = ( 𝐹 ‘ 𝑋 ) )
13	12	3ad2ant3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) = ( 𝐹 ‘ 𝑋 ) )
14	11 13	eqtrd	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ ⟨“ 𝑋 ”⟩ ) = ( 𝐹 ‘ 𝑋 ) )