notrab

Description: Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Assertion	notrab	$⊢ A ∖ \{x \in A \| φ\} = \{x \in A \| \neg φ\}$

Step	Hyp	Ref	Expression
1		difab	$⊢ \{x \| x \in A\} ∖ \{x \| φ\} = \{x \| (x \in A \land \neg φ)\}$
2		difin	$⊢ A ∖ (A \cap \{x \| φ\}) = A ∖ \{x \| φ\}$
3		dfrab3	$⊢ \{x \in A \| φ\} = A \cap \{x \| φ\}$
4	3	difeq2i	$⊢ A ∖ \{x \in A \| φ\} = A ∖ (A \cap \{x \| φ\})$
5		abid2	$⊢ \{x \| x \in A\} = A$
6	5	difeq1i	$⊢ \{x \| x \in A\} ∖ \{x \| φ\} = A ∖ \{x \| φ\}$
7	2 4 6	3eqtr4i	$⊢ A ∖ \{x \in A \| φ\} = \{x \| x \in A\} ∖ \{x \| φ\}$
8		df-rab	$⊢ \{x \in A \| \neg φ\} = \{x \| (x \in A \land \neg φ)\}$
9	1 7 8	3eqtr4i	$⊢ A ∖ \{x \in A \| φ\} = \{x \in A \| \neg φ\}$

Metamath Proof Explorer