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 ( 𝐴 𝑅 𝐵𝑅 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 df-br ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
2 ne0i ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅𝑅 ≠ ∅ )
3 1 2 sylbi ( 𝐴 𝑅 𝐵𝑅 ≠ ∅ )