Theorem mthmi

Description: A statement whose reduct is the reduct of a provable pre-statement is a theorem. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mthmval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
	mthmval.j	$$⊢J=\mathrm{mPPSt}\left(T\right)$$
	mthmval.u	$$⊢U=\mathrm{mThm}\left(T\right)$$
Assertion	mthmi	$$⊢\left(X\in J\wedge R\left(X\right)=R\left(Y\right)\right)\to Y\in U$$

Proof

Step	Hyp	Ref	Expression
1		mthmval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
2		mthmval.j	$$⊢J=\mathrm{mPPSt}\left(T\right)$$
3		mthmval.u	$$⊢U=\mathrm{mThm}\left(T\right)$$
4		fveqeq2	$$⊢x=X\to \left(R\left(x\right)=R\left(Y\right)\leftrightarrow R\left(X\right)=R\left(Y\right)\right)$$
5	4	rspcev	$$⊢\left(X\in J\wedge R\left(X\right)=R\left(Y\right)\right)\to \exists x\in JR\left(x\right)=R\left(Y\right)$$
6	1 2 3	elmthm	$$⊢Y\in U\leftrightarrow \exists x\in JR\left(x\right)=R\left(Y\right)$$
7	5 6	sylibr	$$⊢\left(X\in J\wedge R\left(X\right)=R\left(Y\right)\right)\to Y\in U$$