Metamath Proof Explorer


Theorem eqrelrdv2

Description: A version of eqrelrdv . (Contributed by Rodolfo Medina, 10-Oct-2010)

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

Proof

Step Hyp Ref Expression
1 eqrelrdv2.1
 |-  ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )
2 1 alrimivv
 |-  ( ph -> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) )
3 eqrel
 |-  ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
4 2 3 syl5ibr
 |-  ( ( Rel A /\ Rel B ) -> ( ph -> A = B ) )
5 4 imp
 |-  ( ( ( Rel A /\ Rel B ) /\ ph ) -> A = B )