Theorem vvdifopab

Description: Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019)

	Ref	Expression
Assertion	vvdifopab	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\neg \phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
2	1	notbii	$$⊢\neg ⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \neg \phi$$
3		opelvvdif	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\to \left(⟨x,y⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)\leftrightarrow \neg ⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\right)$$
4	3	el2v	$$⊢⟨x,y⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)\leftrightarrow \neg ⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}$$
5		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\neg \phi \right\}\leftrightarrow \neg \phi$$
6	2 4 5	3bitr4i	$$⊢⟨x,y⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\neg \phi \right\}$$
7	6	gen2	$$⊢\forall x\forall y\left(⟨x,y⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\neg \phi \right\}\right)$$
8		relxp	$$⊢\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)$$
9		reldif	$$⊢\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)$$
10	8 9	ax-mp	$$⊢\mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)$$
11		relopabv	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\neg \phi \right\}$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(\mathrm{V}\times \mathrm{V}\right)$$
13		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\phi \right\}$$
14	12 13	nfdif	$$⊢\underset{\_}{Ⅎ}x\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)$$
15		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\neg \phi \right\}$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}y\left(\mathrm{V}\times \mathrm{V}\right)$$
17		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\phi \right\}$$
18	16 17	nfdif	$$⊢\underset{\_}{Ⅎ}y\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)$$
19		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\neg \phi \right\}$$
20	14 15 18 19	eqrelf	$$⊢\left(\mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)\wedge \mathrm{Rel}\left\{⟨x,y⟩|\neg \phi \right\}\right)\to \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\neg \phi \right\}\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\neg \phi \right\}\right)\right)$$
21	10 11 20	mp2an	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\neg \phi \right\}\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}\right)\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\neg \phi \right\}\right)$$
22	7 21	mpbir	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\neg \phi \right\}$$