This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem notabw

Description: A class abstraction defined by a negation. Version of notab using implicit substitution, which does not require ax-10 , ax-12 . (Contributed by GG, 15-Oct-2024)

		Ref	Expression
	Hypothesis	notabw.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	notabw	$⊢ \{x \| \neg φ\} = V ∖ \{y \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		notabw.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		vex	$⊢ x \in V$
3	2	biantrur	$⊢ \neg x \in \{y \| ψ\} \leftrightarrow (x \in V \land \neg x \in \{y \| ψ\})$
4		df-clab	$⊢ x \in \{y \| ψ\} \leftrightarrow [x/ y] ψ$
5	1	bicomd	$⊢ x = y \to (ψ \leftrightarrow φ)$
6	5	equcoms	$⊢ y = x \to (ψ \leftrightarrow φ)$
7	6	sbievw	$⊢ [x/ y] ψ \leftrightarrow φ$
8	4 7	bitri	$⊢ x \in \{y \| ψ\} \leftrightarrow φ$
9	3 8	xchnxbi	$⊢ \neg φ \leftrightarrow (x \in V \land \neg x \in \{y \| ψ\})$
10	9	abbii	$⊢ \{x \| \neg φ\} = \{x \| (x \in V \land \neg x \in \{y \| ψ\})\}$
11		df-dif	$⊢ V ∖ \{y \| ψ\} = \{x \| (x \in V \land \neg x \in \{y \| ψ\})\}$
12	10 11	eqtr4i	$⊢ \{x \| \neg φ\} = V ∖ \{y \| ψ\}$