Metamath Proof Explorer

Theorem 0er

Description: The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015) (Proof shortened by AV, 1-May-2021)

Ref Expression
Assertion 0er 
|- (/) Er (/)

Proof

Step Hyp Ref Expression
1 rel0 
 |-  Rel (/)
2 df-br 
 |-  ( x (/) y <-> <. x , y >. e. (/) )
3 noel 
 |-  -. <. x , y >. e. (/)
4 3 pm2.21i 
 |-  ( <. x , y >. e. (/) -> y (/) x )
5 2 4 sylbi 
 |-  ( x (/) y -> y (/) x )
6 3 pm2.21i 
 |-  ( <. x , y >. e. (/) -> x (/) z )
7 2 6 sylbi 
 |-  ( x (/) y -> x (/) z )
8 7 adantr 
 |-  ( ( x (/) y /\ y (/) z ) -> x (/) z )
9 noel 
 |-  -. x e. (/)
10 noel 
 |-  -. <. x , x >. e. (/)
11 9 10 2false 
 |-  ( x e. (/) <-> <. x , x >. e. (/) )
12 df-br 
 |-  ( x (/) x <-> <. x , x >. e. (/) )
13 11 12 bitr4i 
 |-  ( x e. (/) <-> x (/) x )
14 1 5 8 13 iseri 
 |-  (/) Er (/)