Theorem exnel

Description: There is always a set not in y . (Contributed by Scott Fenton, 13-Dec-2010)

	Ref	Expression
Assertion	exnel	⊢ ∃ 𝑥 ¬ 𝑥 ∈ 𝑦

Proof

Step	Hyp	Ref	Expression
1		elirrv	⊢ ¬ 𝑦 ∈ 𝑦
2	1	nfth	⊢ Ⅎ 𝑥 ¬ 𝑦 ∈ 𝑦
3		ax8	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑦 ) )
4	3	con3d	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑦 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑦 ) )
5	2 4	spime	⊢ ( ¬ 𝑦 ∈ 𝑦 → ∃ 𝑥 ¬ 𝑥 ∈ 𝑦 )
6	1 5	ax-mp	⊢ ∃ 𝑥 ¬ 𝑥 ∈ 𝑦