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

Metamath Proof Explorer

Theorem eqrel2

Description: Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019)

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

Proof

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