Theorem compne

Description: The complement of A is not equal to A . (Contributed by Andrew Salmon, 15-Jul-2011) (Proof shortened by BJ, 11-Nov-2021)

	Ref	Expression
Assertion	compne	⊢ ( V ∖ 𝐴 ) ≠ 𝐴

Proof

Step	Hyp	Ref	Expression
1		vn0	⊢ V ≠ ∅
2		id	⊢ ( ( V ∖ 𝐴 ) = 𝐴 → ( V ∖ 𝐴 ) = 𝐴 )
3		difeq1	⊢ ( ( V ∖ 𝐴 ) = 𝐴 → ( ( V ∖ 𝐴 ) ∖ 𝐴 ) = ( 𝐴 ∖ 𝐴 ) )
4		difabs	⊢ ( ( V ∖ 𝐴 ) ∖ 𝐴 ) = ( V ∖ 𝐴 )
5		difid	⊢ ( 𝐴 ∖ 𝐴 ) = ∅
6	3 4 5	3eqtr3g	⊢ ( ( V ∖ 𝐴 ) = 𝐴 → ( V ∖ 𝐴 ) = ∅ )
7	2 6	eqtr3d	⊢ ( ( V ∖ 𝐴 ) = 𝐴 → 𝐴 = ∅ )
8	7	difeq2d	⊢ ( ( V ∖ 𝐴 ) = 𝐴 → ( V ∖ 𝐴 ) = ( V ∖ ∅ ) )
9		dif0	⊢ ( V ∖ ∅ ) = V
10	8 9	eqtrdi	⊢ ( ( V ∖ 𝐴 ) = 𝐴 → ( V ∖ 𝐴 ) = V )
11	10 6	eqtr3d	⊢ ( ( V ∖ 𝐴 ) = 𝐴 → V = ∅ )
12	11	necon3i	⊢ ( V ≠ ∅ → ( V ∖ 𝐴 ) ≠ 𝐴 )
13	1 12	ax-mp	⊢ ( V ∖ 𝐴 ) ≠ 𝐴