Theorem elnev

Description: Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011)

	Ref	Expression
Assertion	elnev	⊢ ( 𝐴 ∈ V ↔ { 𝑥 ∣ ¬ 𝑥 = 𝐴 } ≠ V )

Proof

Step	Hyp	Ref	Expression
1		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
2		df-v	⊢ V = { 𝑥 ∣ 𝑥 = 𝑥 }
3	2	eqeq2i	⊢ ( { 𝑥 ∣ ¬ 𝑥 = 𝐴 } = V ↔ { 𝑥 ∣ ¬ 𝑥 = 𝐴 } = { 𝑥 ∣ 𝑥 = 𝑥 } )
4		equid	⊢ 𝑥 = 𝑥
5	4	tbt	⊢ ( ¬ 𝑥 = 𝐴 ↔ ( ¬ 𝑥 = 𝐴 ↔ 𝑥 = 𝑥 ) )
6	5	albii	⊢ ( ∀ 𝑥 ¬ 𝑥 = 𝐴 ↔ ∀ 𝑥 ( ¬ 𝑥 = 𝐴 ↔ 𝑥 = 𝑥 ) )
7		alnex	⊢ ( ∀ 𝑥 ¬ 𝑥 = 𝐴 ↔ ¬ ∃ 𝑥 𝑥 = 𝐴 )
8		abbi	⊢ ( ∀ 𝑥 ( ¬ 𝑥 = 𝐴 ↔ 𝑥 = 𝑥 ) ↔ { 𝑥 ∣ ¬ 𝑥 = 𝐴 } = { 𝑥 ∣ 𝑥 = 𝑥 } )
9	6 7 8	3bitr3ri	⊢ ( { 𝑥 ∣ ¬ 𝑥 = 𝐴 } = { 𝑥 ∣ 𝑥 = 𝑥 } ↔ ¬ ∃ 𝑥 𝑥 = 𝐴 )
10	3 9	bitri	⊢ ( { 𝑥 ∣ ¬ 𝑥 = 𝐴 } = V ↔ ¬ ∃ 𝑥 𝑥 = 𝐴 )
11	10	necon2abii	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ { 𝑥 ∣ ¬ 𝑥 = 𝐴 } ≠ V )
12	1 11	bitri	⊢ ( 𝐴 ∈ V ↔ { 𝑥 ∣ ¬ 𝑥 = 𝐴 } ≠ V )