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	$$⊢R=\mathrm{mStRed}\left(T\right)$$
	mthmb.u	$$⊢U=\mathrm{mThm}\left(T\right)$$
Assertion	mthmb	$$⊢R\left(X\right)=R\left(Y\right)\to \left(X\in U\leftrightarrow Y\in U\right)$$

Proof

Step	Hyp	Ref	Expression
1		mthmb.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
2		mthmb.u	$$⊢U=\mathrm{mThm}\left(T\right)$$
3	1 2	mthmblem	$$⊢R\left(X\right)=R\left(Y\right)\to \left(X\in U\to Y\in U\right)$$
4	1 2	mthmblem	$$⊢R\left(Y\right)=R\left(X\right)\to \left(Y\in U\to X\in U\right)$$
5	4	eqcoms	$$⊢R\left(X\right)=R\left(Y\right)\to \left(Y\in U\to X\in U\right)$$
6	3 5	impbid	$$⊢R\left(X\right)=R\left(Y\right)\to \left(X\in U\leftrightarrow Y\in U\right)$$