Metamath Proof Explorer

Theorem abnex

Description: Sufficient condition for a class abstraction to be a proper class. Lemma for snnex and pwnex . See the comment of abnexg . (Contributed by BJ, 2-May-2021)

		Ref	Expression
	Assertion	abnex	$⊢ \forall x (F \in V \land x \in F) \to \neg \{y \| \exists x y = F\} \in V$

Proof

Step	Hyp	Ref	Expression
1		vprc	$⊢ \neg V \in V$
2		alral	$⊢ \forall x (F \in V \land x \in F) \to \forall x \in V (F \in V \land x \in F)$
3		rexv	$⊢ \exists x \in V y = F \leftrightarrow \exists x y = F$
4	3	bicomi	$⊢ \exists x y = F \leftrightarrow \exists x \in V y = F$
5	4	abbii	$⊢ \{y \| \exists x y = F\} = \{y \| \exists x \in V y = F\}$
6	5	eleq1i	$⊢ \{y \| \exists x y = F\} \in V \leftrightarrow \{y \| \exists x \in V y = F\} \in V$
7	6	biimpi	$⊢ \{y \| \exists x y = F\} \in V \to \{y \| \exists x \in V y = F\} \in V$
8		abnexg	$⊢ \forall x \in V (F \in V \land x \in F) \to (\{y \| \exists x \in V y = F\} \in V \to V \in V)$
9	2 7 8	syl2im	$⊢ \forall x (F \in V \land x \in F) \to (\{y \| \exists x y = F\} \in V \to V \in V)$
10	1 9	mtoi	$⊢ \forall x (F \in V \land x \in F) \to \neg \{y \| \exists x y = F\} \in V$