Metamath Proof Explorer

Theorem br0

Description: The empty binary relation never holds. (Contributed by NM, 23-Aug-2018)

Ref Expression
Assertion br0 
|- -. A (/) B

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. <. A , B >. e. (/)
2 df-br 
 |-  ( A (/) B <-> <. A , B >. e. (/) )
3 1 2 mtbir 
 |-  -. A (/) B