notzfaus

Description: In the Separation Scheme zfauscl , we require that y not occur in ph (which can be generalized to "not be free in"). Here we show special cases of A and ph that result in a contradiction if that requirement is not met. (Contributed by NM, 8-Feb-2006) (Proof shortened by BJ, 18-Nov-2023)

	Ref	Expression
Hypotheses	notzfaus.1	$⊢ A = \{\emptyset\}$
	notzfaus.2	$⊢ φ \leftrightarrow \neg x \in y$
Assertion	notzfaus	$⊢ \neg \exists y \forall x (x \in y \leftrightarrow (x \in A \land φ))$

Proof

Step	Hyp	Ref	Expression
1		notzfaus.1	$⊢ A = \{\emptyset\}$
2		notzfaus.2	$⊢ φ \leftrightarrow \neg x \in y$
3		0ex	$⊢ \emptyset \in V$
4	3	snnz	$⊢ \{\emptyset\} \neq \emptyset$
5	1 4	eqnetri	$⊢ A \neq \emptyset$
6		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
7	5 6	mpbi	$⊢ \exists x x \in A$
8		pm5.19	$⊢ \neg (x \in y \leftrightarrow \neg x \in y)$
9		ibar	$⊢ x \in A \to (φ \leftrightarrow (x \in A \land φ))$
10	9 2	bitr3di	$⊢ x \in A \to ((x \in A \land φ) \leftrightarrow \neg x \in y)$
11	10	bibi2d	$⊢ x \in A \to ((x \in y \leftrightarrow (x \in A \land φ)) \leftrightarrow (x \in y \leftrightarrow \neg x \in y))$
12	8 11	mtbiri	$⊢ x \in A \to \neg (x \in y \leftrightarrow (x \in A \land φ))$
13	7 12	eximii	$⊢ \exists x \neg (x \in y \leftrightarrow (x \in A \land φ))$
14		exnal	$⊢ \exists x \neg (x \in y \leftrightarrow (x \in A \land φ)) \leftrightarrow \neg \forall x (x \in y \leftrightarrow (x \in A \land φ))$
15	13 14	mpbi	$⊢ \neg \forall x (x \in y \leftrightarrow (x \in A \land φ))$
16	15	nex	$⊢ \neg \exists y \forall x (x \in y \leftrightarrow (x \in A \land φ))$

Metamath Proof Explorer

Theorem notzfaus

Proof