Theorem brvdif2

Description: Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018)

	Ref	Expression
Assertion	brvdif2	$$⊢A\left(\mathrm{V}\setminus R\right)B\leftrightarrow \neg ⟨A,B⟩\in R$$

Proof

Step	Hyp	Ref	Expression
1		brvdif	$$⊢A\left(\mathrm{V}\setminus R\right)B\leftrightarrow \neg ARB$$
2		df-br	$$⊢ARB\leftrightarrow ⟨A,B⟩\in R$$
3	1 2	xchbinx	$$⊢A\left(\mathrm{V}\setminus R\right)B\leftrightarrow \neg ⟨A,B⟩\in R$$