Metamath Proof Explorer

Theorem dfer2

Description: Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion dfer2 
|- ( R Er A <-> ( Rel R /\ dom R = A /\ A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )

Proof

Step Hyp Ref Expression
1 df-er 
 |-  ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
2 cnvsym 
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )
3 cotr 
 |-  ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
4 2 3 anbi12i 
 |-  ( ( `' R C_ R /\ ( R o. R ) C_ R ) <-> ( A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) )
5 unss 
 |-  ( ( `' R C_ R /\ ( R o. R ) C_ R ) <-> ( `' R u. ( R o. R ) ) C_ R )
6 19.28v 
 |-  ( A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> ( ( x R y -> y R x ) /\ A. z ( ( x R y /\ y R z ) -> x R z ) ) )
7 6 albii 
 |-  ( A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. y ( ( x R y -> y R x ) /\ A. z ( ( x R y /\ y R z ) -> x R z ) ) )
8 19.26 
 |-  ( A. y ( ( x R y -> y R x ) /\ A. z ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. y ( x R y -> y R x ) /\ A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) )
9 7 8 bitri 
 |-  ( A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. y ( x R y -> y R x ) /\ A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) )
10 9 albii 
 |-  ( A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x ( A. y ( x R y -> y R x ) /\ A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) )
11 19.26 
 |-  ( A. x ( A. y ( x R y -> y R x ) /\ A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) )
12 10 11 bitr2i 
 |-  ( ( A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) )
13 4 5 12 3bitr3i 
 |-  ( ( `' R u. ( R o. R ) ) C_ R <-> A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) )
14 13 3anbi3i 
 |-  ( ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) <-> ( Rel R /\ dom R = A /\ A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
15 1 14 bitri 
 |-  ( R Er A <-> ( Rel R /\ dom R = A /\ A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )