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 = ( mStRed ` T )
	mthmb.u	|- U = ( mThm ` T )
Assertion	mthmb	|- ( ( R ` X ) = ( R ` Y ) -> ( X e. U <-> Y e. U ) )

Proof

Step	Hyp	Ref	Expression
1		mthmb.r	|- R = ( mStRed ` T )
2		mthmb.u	|- U = ( mThm ` T )
3	1 2	mthmblem	|- ( ( R ` X ) = ( R ` Y ) -> ( X e. U -> Y e. U ) )
4	1 2	mthmblem	|- ( ( R ` Y ) = ( R ` X ) -> ( Y e. U -> X e. U ) )
5	4	eqcoms	|- ( ( R ` X ) = ( R ` Y ) -> ( Y e. U -> X e. U ) )
6	3 5	impbid	|- ( ( R ` X ) = ( R ` Y ) -> ( X e. U <-> Y e. U ) )