Theorem brvvdif

Description: Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018)

	Ref	Expression
Assertion	brvvdif	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus R\right)B\leftrightarrow \neg ARB\right)$$

Proof

Step	Hyp	Ref	Expression
1		opelvvdif	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus R\right)\leftrightarrow \neg ⟨A,B⟩\in R\right)$$
2		df-br	$$⊢A\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus R\right)B\leftrightarrow ⟨A,B⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus R\right)$$
3		df-br	$$⊢ARB\leftrightarrow ⟨A,B⟩\in R$$
4	3	notbii	$$⊢\neg ARB\leftrightarrow \neg ⟨A,B⟩\in R$$
5	1 2 4	3bitr4g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus R\right)B\leftrightarrow \neg ARB\right)$$