Theorem cnveqb

Description: Equality theorem for converse. (Contributed by FL, 19-Sep-2011)

	Ref	Expression
Assertion	cnveqb	|- ( ( Rel A /\ Rel B ) -> ( A = B <-> `' A = `' B ) )

Proof

Step	Hyp	Ref	Expression
1		cnvssb	|- ( Rel A -> ( A C_ B <-> `' A C_ `' B ) )
2		cnvssb	|- ( Rel B -> ( B C_ A <-> `' B C_ `' A ) )
3	1 2	bi2anan9	|- ( ( Rel A /\ Rel B ) -> ( ( A C_ B /\ B C_ A ) <-> ( `' A C_ `' B /\ `' B C_ `' A ) ) )
4		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss	|- ( `' A = `' B <-> ( `' A C_ `' B /\ `' B C_ `' A ) )
6	3 4 5	3bitr4g	|- ( ( Rel A /\ Rel B ) -> ( A = B <-> `' A = `' B ) )