Metamath Proof Explorer

Theorem brne0

Description: If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018)

Ref Expression
Assertion brne0 
|- ( A R B -> R =/= (/) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( A R B <-> <. A , B >. e. R )
2 ne0i 
 |-  ( <. A , B >. e. R -> R =/= (/) )
3 1 2 sylbi 
 |-  ( A R B -> R =/= (/) )