Theorem eqrel

Description: Extensionality principle for relations. Theorem 3.2(ii) of Monk1 p. 33. (Contributed by NM, 2-Aug-1994)

	Ref	Expression
Assertion	eqrel	|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssrel	|- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
2		ssrel	|- ( Rel B -> ( B C_ A <-> A. x A. y ( <. x , y >. e. B -> <. x , y >. e. A ) ) )
3	1 2	bi2anan9	|- ( ( Rel A /\ Rel B ) -> ( ( A C_ B /\ B C_ A ) <-> ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) /\ A. x A. y ( <. x , y >. e. B -> <. x , y >. e. A ) ) ) )
4		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		2albiim	|- ( A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) <-> ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) /\ A. x A. y ( <. x , y >. e. B -> <. x , y >. e. A ) ) )
6	3 4 5	3bitr4g	|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )