Theorem noelOLD

Description: Obsolete version of noel as of 11-Oct-2026. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	noelOLD	⊢ ¬ 𝐴 ∈ ∅

Proof

Step	Hyp	Ref	Expression
1		nsb	⊢ ( ∀ 𝑦 ¬ ⊥ → ¬ [ 𝑥 / 𝑦 ] ⊥ )
2		fal	⊢ ¬ ⊥
3	1 2	mpg	⊢ ¬ [ 𝑥 / 𝑦 ] ⊥
4		dfnul4	⊢ ∅ = { 𝑦 ∣ ⊥ }
5	4	eleq2i	⊢ ( 𝑥 ∈ ∅ ↔ 𝑥 ∈ { 𝑦 ∣ ⊥ } )
6		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ ⊥ } ↔ [ 𝑥 / 𝑦 ] ⊥ )
7	5 6	bitri	⊢ ( 𝑥 ∈ ∅ ↔ [ 𝑥 / 𝑦 ] ⊥ )
8	3 7	mtbir	⊢ ¬ 𝑥 ∈ ∅
9	8	intnan	⊢ ¬ ( 𝑥 = 𝐴 ∧ 𝑥 ∈ ∅ )
10	9	nex	⊢ ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ ∅ )
11		dfclel	⊢ ( 𝐴 ∈ ∅ ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ ∅ ) )
12	10 11	mtbir	⊢ ¬ 𝐴 ∈ ∅