Theorem msubrsub

Description: A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	msubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	msubffval.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
	msubffval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	msubffval.o	⊢ 𝑂 = ( mRSubst ‘ 𝑇 )
Assertion	msubrsub	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( 2nd ‘ ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		msubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		msubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		msubffval.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
4		msubffval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
5		msubffval.o	⊢ 𝑂 = ( mRSubst ‘ 𝑇 )
6	1 2 3 4 5	msubval	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = ⟨ ( 1st ‘ 𝑋 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) ⟩ )
7		fvex	⊢ ( 1st ‘ 𝑋 ) ∈ V
8		fvex	⊢ ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) ∈ V
9	7 8	op2ndd	⊢ ( ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = ⟨ ( 1st ‘ 𝑋 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) ⟩ → ( 2nd ‘ ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) )
10	6 9	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( 2nd ‘ ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) )