difopab

Description: Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015) (Proof shortened by SN, 19-Dec-2024)

		Ref	Expression
	Assertion	difopab	$⊢ \{⟨x, y⟩ \| φ\} ∖ \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| (φ \land \neg ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		relopabv	$⊢ Rel \{⟨x, y⟩ \| φ\}$
2		reldif	$⊢ Rel \{⟨x, y⟩ \| φ\} \to Rel (\{⟨x, y⟩ \| φ\} ∖ \{⟨x, y⟩ \| ψ\})$
3	1 2	ax-mp	$⊢ Rel (\{⟨x, y⟩ \| φ\} ∖ \{⟨x, y⟩ \| ψ\})$
4		relopabv	$⊢ Rel \{⟨x, y⟩ \| (φ \land \neg ψ)\}$
5		sban	$⊢ [z/ x] ([w/ y] φ \land [w/ y] \neg ψ) \leftrightarrow ([z/ x] [w/ y] φ \land [z/ x] [w/ y] \neg ψ)$
6		sban	$⊢ [w/ y] (φ \land \neg ψ) \leftrightarrow ([w/ y] φ \land [w/ y] \neg ψ)$
7	6	sbbii	$⊢ [z/ x] [w/ y] (φ \land \neg ψ) \leftrightarrow [z/ x] ([w/ y] φ \land [w/ y] \neg ψ)$
8		vopelopabsb	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow [z/ x] [w/ y] φ$
9		sbn	$⊢ [z/ x] \neg [w/ y] ψ \leftrightarrow \neg [z/ x] [w/ y] ψ$
10		sbn	$⊢ [w/ y] \neg ψ \leftrightarrow \neg [w/ y] ψ$
11	10	sbbii	$⊢ [z/ x] [w/ y] \neg ψ \leftrightarrow [z/ x] \neg [w/ y] ψ$
12		vopelopabsb	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\} \leftrightarrow [z/ x] [w/ y] ψ$
13	12	notbii	$⊢ \neg ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\} \leftrightarrow \neg [z/ x] [w/ y] ψ$
14	9 11 13	3bitr4ri	$⊢ \neg ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\} \leftrightarrow [z/ x] [w/ y] \neg ψ$
15	8 14	anbi12i	$⊢ (⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \land \neg ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\}) \leftrightarrow ([z/ x] [w/ y] φ \land [z/ x] [w/ y] \neg ψ)$
16	5 7 15	3bitr4ri	$⊢ (⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \land \neg ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\}) \leftrightarrow [z/ x] [w/ y] (φ \land \neg ψ)$
17		eldif	$⊢ ⟨z, w⟩ \in (\{⟨x, y⟩ \| φ\} ∖ \{⟨x, y⟩ \| ψ\}) \leftrightarrow (⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \land \neg ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\})$
18		vopelopabsb	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| (φ \land \neg ψ)\} \leftrightarrow [z/ x] [w/ y] (φ \land \neg ψ)$
19	16 17 18	3bitr4i	$⊢ ⟨z, w⟩ \in (\{⟨x, y⟩ \| φ\} ∖ \{⟨x, y⟩ \| ψ\}) \leftrightarrow ⟨z, w⟩ \in \{⟨x, y⟩ \| (φ \land \neg ψ)\}$
20	3 4 19	eqrelriiv	$⊢ \{⟨x, y⟩ \| φ\} ∖ \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| (φ \land \neg ψ)\}$

Metamath Proof Explorer

Theorem difopab

Proof