This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )