Metamath Proof Explorer

Theorem notzfausOLD

Description: Obsolete proof of notzfaus as of 18-Nov-2023. (Contributed by NM, 8-Feb-2006) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	notzfaus.1	$⊢ A = \{\emptyset\}$
		notzfaus.2	$⊢ φ \leftrightarrow \neg x \in y$
	Assertion	notzfausOLD	$⊢ \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		biimt	$⊢ x \in A \to (x \in y \leftrightarrow (x \in A \to x \in y))$
9		iman	$⊢ (x \in A \to x \in y) \leftrightarrow \neg (x \in A \land \neg x \in y)$
10	2	anbi2i	$⊢ (x \in A \land φ) \leftrightarrow (x \in A \land \neg x \in y)$
11	9 10	xchbinxr	$⊢ (x \in A \to x \in y) \leftrightarrow \neg (x \in A \land φ)$
12	8 11	bitrdi	$⊢ x \in A \to (x \in y \leftrightarrow \neg (x \in A \land φ))$
13		xor3	$⊢ \neg (x \in y \leftrightarrow (x \in A \land φ)) \leftrightarrow (x \in y \leftrightarrow \neg (x \in A \land φ))$
14	12 13	sylibr	$⊢ x \in A \to \neg (x \in y \leftrightarrow (x \in A \land φ))$
15	7 14	eximii	$⊢ \exists x \neg (x \in y \leftrightarrow (x \in A \land φ))$
16		exnal	$⊢ \exists x \neg (x \in y \leftrightarrow (x \in A \land φ)) \leftrightarrow \neg \forall x (x \in y \leftrightarrow (x \in A \land φ))$
17	15 16	mpbi	$⊢ \neg \forall x (x \in y \leftrightarrow (x \in A \land φ))$
18	17	nex	$⊢ \neg \exists y \forall x (x \in y \leftrightarrow (x \in A \land φ))$