Theorem mthmb

Description: If two statements have the same reduct then one is a theorem iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mthmb.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	mthmb.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
Assertion	mthmb	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		mthmb.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2		mthmb.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
3	1 2	mthmblem	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑈 → 𝑌 ∈ 𝑈 ) )
4	1 2	mthmblem	⊢ ( ( 𝑅 ‘ 𝑌 ) = ( 𝑅 ‘ 𝑋 ) → ( 𝑌 ∈ 𝑈 → 𝑋 ∈ 𝑈 ) )
5	4	eqcoms	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑌 ∈ 𝑈 → 𝑋 ∈ 𝑈 ) )
6	3 5	impbid	⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈 ) )