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	⊢ 𝐴 = { ∅ }
	notsep.2	⊢ ( 𝜑 ↔ ¬ 𝑥 ∈ 𝑦 )
Assertion	notsep	⊢ ¬ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		notsep.1	⊢ 𝐴 = { ∅ }
2		notsep.2	⊢ ( 𝜑 ↔ ¬ 𝑥 ∈ 𝑦 )
3		0ex	⊢ ∅ ∈ V
4	3	snnz	⊢ { ∅ } ≠ ∅
5	1 4	eqnetri	⊢ 𝐴 ≠ ∅
6		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
7	5 6	mpbi	⊢ ∃ 𝑥 𝑥 ∈ 𝐴
8		pm5.19	⊢ ¬ ( 𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑦 )
9		ibar	⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
10	9 2	bitr3di	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ¬ 𝑥 ∈ 𝑦 ) )
11	10	bibi2d	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑦 ) ) )
12	8 11	mtbiri	⊢ ( 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
13	7 12	eximii	⊢ ∃ 𝑥 ¬ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
14		exnal	⊢ ( ∃ 𝑥 ¬ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
15	13 14	mpbi	⊢ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
16	15	nex	⊢ ¬ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )