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

Proof

Step	Hyp	Ref	Expression
1		notzfaus.1	⊢ 𝐴 = { ∅ }
2		notzfaus.2	⊢ ( 𝜑 ↔ ¬ 𝑥 ∈ 𝑦 )
3		0ex	⊢ ∅ ∈ V
4	3	snnz	⊢ { ∅ } ≠ ∅
5	1 4	eqnetri	⊢ 𝐴 ≠ ∅
6		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
7	5 6	mpbi	⊢ ∃ 𝑥 𝑥 ∈ 𝐴
8		biimt	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) ) )
9		iman	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝑦 ) )
10	2	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝑦 ) )
11	9 10	xchbinxr	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
12	8 11	bitrdi	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
13		xor3	⊢ ( ¬ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
14	12 13	sylibr	⊢ ( 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
15	7 14	eximii	⊢ ∃ 𝑥 ¬ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
16		exnal	⊢ ( ∃ 𝑥 ¬ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
17	15 16	mpbi	⊢ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
18	17	nex	⊢ ¬ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )