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 = ( mStRed ` T )
	mthmval.j	|- J = ( mPPSt ` T )
	mthmval.u	|- U = ( mThm ` T )
Assertion	mthmi	|- ( ( X e. J /\ ( R ` X ) = ( R ` Y ) ) -> Y e. U )

Proof

Step	Hyp	Ref	Expression
1		mthmval.r	|- R = ( mStRed ` T )
2		mthmval.j	|- J = ( mPPSt ` T )
3		mthmval.u	|- U = ( mThm ` T )
4		fveqeq2	|- ( x = X -> ( ( R ` x ) = ( R ` Y ) <-> ( R ` X ) = ( R ` Y ) ) )
5	4	rspcev	|- ( ( X e. J /\ ( R ` X ) = ( R ` Y ) ) -> E. x e. J ( R ` x ) = ( R ` Y ) )
6	1 2 3	elmthm	|- ( Y e. U <-> E. x e. J ( R ` x ) = ( R ` Y ) )
7	5 6	sylibr	|- ( ( X e. J /\ ( R ` X ) = ( R ` Y ) ) -> Y e. U )