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 | ⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈 ) ) |
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 | ⊢ ( ( 𝑅 ‘ 𝑋 ) = ( 𝑅 ‘ 𝑌 ) → ( 𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈 ) ) |