Theorem opelvvdif

Description: Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		eldif	$$⊢⟨A,B⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus R\right)\leftrightarrow \left(⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \neg ⟨A,B⟩\in R\right)$$
2		opelvvg	$$⊢\left(A\in V\wedge B\in W\right)\to ⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
3	2	biantrurd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg ⟨A,B⟩\in R\leftrightarrow \left(⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \neg ⟨A,B⟩\in R\right)\right)$$
4	1 3	bitr4id	$$⊢\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)$$