Theorem 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=\left\{\varnothing \right\}$$
	notzfaus.2	$$⊢\phi \leftrightarrow \neg x\in y$$
Assertion	notzfaus	$$⊢\neg \exists y\forall x\left(x\in y\leftrightarrow \left(x\in A\wedge \phi \right)\right)$$

Proof

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