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	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	mthmval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
	mthmval.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
Assertion	mthmi	⊢ ( ( 𝑋 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) ) → 𝑌 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mthmval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2		mthmval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
3		mthmval.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
4		fveqeq2	⊢ ( 𝑥 = 𝑋 → ( ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑌 ) ↔ ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) ) )
5	4	rspcev	⊢ ( ( 𝑋 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑌 ) )
6	1 2 3	elmthm	⊢ ( 𝑌 ∈ 𝑈 ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑌 ) )
7	5 6	sylibr	⊢ ( ( 𝑋 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) ) → 𝑌 ∈ 𝑈 )