Theorem notsep

Description: In the Separation Scheme sepgi , we require that y not occur in ph (which can be generalized to "not be free in"). That requirement is necessary: notsep , which requires only ax-ext and ax-nul on top of first-order logic, derives *non*-existence of a "separating set" for specific values of the containing set A and of the separating condition ph . Therefore, from the axioms required by notsep and an overly strong axiom of separation without the requirement that y not occur in ph , we could derive F. , a contradiction. (Contributed by NM, 8-Feb-2006) (Proof shortened by BJ, 18-Nov-2023)

	Ref	Expression
Hypotheses	notsep.1	|- A = { (/) }
	notsep.2	|- ( ph <-> -. x e. y )
Assertion	notsep	|- -. E. y A. x ( x e. y <-> ( x e. A /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		notsep.1	|- A = { (/) }
2		notsep.2	|- ( ph <-> -. x e. y )
3		0ex	|- (/) e. _V
4	3	snnz	|- { (/) } =/= (/)
5	1 4	eqnetri	|- A =/= (/)
6		n0	|- ( A =/= (/) <-> E. x x e. A )
7	5 6	mpbi	|- E. x x e. A
8		pm5.19	|- -. ( x e. y <-> -. x e. y )
9		ibar	|- ( x e. A -> ( ph <-> ( x e. A /\ ph ) ) )
10	9 2	bitr3di	|- ( x e. A -> ( ( x e. A /\ ph ) <-> -. x e. y ) )
11	10	bibi2d	|- ( x e. A -> ( ( x e. y <-> ( x e. A /\ ph ) ) <-> ( x e. y <-> -. x e. y ) ) )
12	8 11	mtbiri	|- ( x e. A -> -. ( x e. y <-> ( x e. A /\ ph ) ) )
13	7 12	eximii	|- E. x -. ( x e. y <-> ( x e. A /\ ph ) )
14		exnal	|- ( E. x -. ( x e. y <-> ( x e. A /\ ph ) ) <-> -. A. x ( x e. y <-> ( x e. A /\ ph ) ) )
15	13 14	mpbi	|- -. A. x ( x e. y <-> ( x e. A /\ ph ) )
16	15	nex	|- -. E. y A. x ( x e. y <-> ( x e. A /\ ph ) )