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 | ⊢ ( 𝐴 𝑅 𝐵 → 𝑅 ≠ ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br | ⊢ ( 𝐴 𝑅 𝐵 ↔ 〈 𝐴 , 𝐵 〉 ∈ 𝑅 ) | |
2 | ne0i | ⊢ ( 〈 𝐴 , 𝐵 〉 ∈ 𝑅 → 𝑅 ≠ ∅ ) | |
3 | 1 2 | sylbi | ⊢ ( 𝐴 𝑅 𝐵 → 𝑅 ≠ ∅ ) |