Theorem br0

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

	Ref	Expression
Assertion	br0	$$⊢\neg A\varnothing B$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg ⟨A,B⟩\in \varnothing$$
2		df-br	$$⊢A\varnothing B\leftrightarrow ⟨A,B⟩\in \varnothing$$
3	1 2	mtbir	$$⊢\neg A\varnothing B$$