Theorem mrsubvr

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

	Ref	Expression
Hypotheses	mrsubvr.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
	mrsubvr.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
	mrsubvr.s	$$⊢S=\mathrm{mRSubst}\left(T\right)$$
Assertion	mrsubvr	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in A\right)\to S\left(F\right)\left(⟨“X”⟩\right)=F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		mrsubvr.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		mrsubvr.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
3		mrsubvr.s	$$⊢S=\mathrm{mRSubst}\left(T\right)$$
4		ssun2	$$⊢V\subseteq \mathrm{mCN}\left(T\right)\cup V$$
5		simp2	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in A\right)\to A\subseteq V$$
6		simp3	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in A\right)\to X\in A$$
7	5 6	sseldd	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in A\right)\to X\in V$$
8	4 7	sseldi	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in A\right)\to X\in \left(\mathrm{mCN}\left(T\right)\cup V\right)$$
9		eqid	$$⊢\mathrm{mCN}\left(T\right)=\mathrm{mCN}\left(T\right)$$
10	9 1 2 3	mrsubcv	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in \left(\mathrm{mCN}\left(T\right)\cup V\right)\right)\to S\left(F\right)\left(⟨“X”⟩\right)=if\left(X\in A,F\left(X\right),⟨“X”⟩\right)$$
11	8 10	syld3an3	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in A\right)\to S\left(F\right)\left(⟨“X”⟩\right)=if\left(X\in A,F\left(X\right),⟨“X”⟩\right)$$
12		iftrue	$$⊢X\in A\to if\left(X\in A,F\left(X\right),⟨“X”⟩\right)=F\left(X\right)$$
13	12	3ad2ant3	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in A\right)\to if\left(X\in A,F\left(X\right),⟨“X”⟩\right)=F\left(X\right)$$
14	11 13	eqtrd	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in A\right)\to S\left(F\right)\left(⟨“X”⟩\right)=F\left(X\right)$$