Theorem difopab

Description: Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015)

	Ref	Expression
Assertion	difopab	$$⊢\left\{⟨x,y⟩|\phi \right\}\setminus \left\{⟨x,y⟩|\psi \right\}=\left\{⟨x,y⟩|\left(\phi \wedge \neg \psi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		relopabv	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}$$
2		reldif	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}\to \mathrm{Rel}\left(\left\{⟨x,y⟩|\phi \right\}\setminus \left\{⟨x,y⟩|\psi \right\}\right)$$
3	1 2	ax-mp	$$⊢\mathrm{Rel}\left(\left\{⟨x,y⟩|\phi \right\}\setminus \left\{⟨x,y⟩|\psi \right\}\right)$$
4		relopabv	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\left(\phi \wedge \neg \psi \right)\right\}$$
5		sbcan	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi \right)$$
6		sbcan	$$⊢\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\left(\phi \wedge \neg \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi \right)$$
7	6	sbcbii	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\left(\phi \wedge \neg \psi \right)\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi \right)$$
8		opelopabsb	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi$$
9		sbcng	$$⊢z\in \mathrm{V}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \leftrightarrow \neg \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \right)$$
10	9	elv	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \leftrightarrow \neg \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi$$
11		sbcng	$$⊢w\in \mathrm{V}\to \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi \leftrightarrow \neg \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \right)$$
12	11	elv	$$⊢\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi \leftrightarrow \neg \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi$$
13	12	sbcbii	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi$$
14		opelopabsb	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|\psi \right\}\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi$$
15	14	notbii	$$⊢\neg ⟨z,w⟩\in \left\{⟨x,y⟩|\psi \right\}\leftrightarrow \neg \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi$$
16	10 13 15	3bitr4ri	$$⊢\neg ⟨z,w⟩\in \left\{⟨x,y⟩|\psi \right\}\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi$$
17	8 16	anbi12i	$$⊢\left(⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\wedge \neg ⟨z,w⟩\in \left\{⟨x,y⟩|\psi \right\}\right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\neg \psi \right)$$
18	5 7 17	3bitr4ri	$$⊢\left(⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\wedge \neg ⟨z,w⟩\in \left\{⟨x,y⟩|\psi \right\}\right)\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\left(\phi \wedge \neg \psi \right)$$
19		eldif	$$⊢⟨z,w⟩\in \left(\left\{⟨x,y⟩|\phi \right\}\setminus \left\{⟨x,y⟩|\psi \right\}\right)\leftrightarrow \left(⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\wedge \neg ⟨z,w⟩\in \left\{⟨x,y⟩|\psi \right\}\right)$$
20		opelopabsb	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|\left(\phi \wedge \neg \psi \right)\right\}\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\left(\phi \wedge \neg \psi \right)$$
21	18 19 20	3bitr4i	$$⊢⟨z,w⟩\in \left(\left\{⟨x,y⟩|\phi \right\}\setminus \left\{⟨x,y⟩|\psi \right\}\right)\leftrightarrow ⟨z,w⟩\in \left\{⟨x,y⟩|\left(\phi \wedge \neg \psi \right)\right\}$$
22	3 4 21	eqrelriiv	$$⊢\left\{⟨x,y⟩|\phi \right\}\setminus \left\{⟨x,y⟩|\psi \right\}=\left\{⟨x,y⟩|\left(\phi \wedge \neg \psi \right)\right\}$$