Theorem compne 37665

Description: The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.)

Assertion

Ref	Expression
compne	⊢ (V ∖ 𝐴) ≠ 𝐴

Proof of Theorem compne

Step	Hyp	Ref	Expression
1		vn0 3883	. 2 ⊢ V ≠ ∅
2		ssun1 3738	. . . . . . . 8 ⊢ V ⊆ (V ∪ 𝐴)
3		ssv 3588	. . . . . . . 8 ⊢ (V ∪ 𝐴) ⊆ V
4	2, 3	eqssi 3584	. . . . . . 7 ⊢ V = (V ∪ 𝐴)
5		undif1 3995	. . . . . . 7 ⊢ ((V ∖ 𝐴) ∪ 𝐴) = (V ∪ 𝐴)
6	4, 5	eqtr4i 2635	. . . . . 6 ⊢ V = ((V ∖ 𝐴) ∪ 𝐴)
7		uneq1 3722	. . . . . 6 ⊢ ((V ∖ 𝐴) = 𝐴 → ((V ∖ 𝐴) ∪ 𝐴) = (𝐴 ∪ 𝐴))
8	6, 7	syl5eq 2656	. . . . 5 ⊢ ((V ∖ 𝐴) = 𝐴 → V = (𝐴 ∪ 𝐴))
9		unidm 3718	. . . . 5 ⊢ (𝐴 ∪ 𝐴) = 𝐴
10	8, 9	syl6eq 2660	. . . 4 ⊢ ((V ∖ 𝐴) = 𝐴 → V = 𝐴)
11		difabs 3851	. . . . . . 7 ⊢ ((V ∖ 𝐴) ∖ 𝐴) = (V ∖ 𝐴)
12		id 22	. . . . . . 7 ⊢ ((V ∖ 𝐴) = 𝐴 → (V ∖ 𝐴) = 𝐴)
13	11, 12	syl5req 2657	. . . . . 6 ⊢ ((V ∖ 𝐴) = 𝐴 → 𝐴 = ((V ∖ 𝐴) ∖ 𝐴))
14		difeq1 3683	. . . . . 6 ⊢ ((V ∖ 𝐴) = 𝐴 → ((V ∖ 𝐴) ∖ 𝐴) = (𝐴 ∖ 𝐴))
15	13, 14	eqtrd 2644	. . . . 5 ⊢ ((V ∖ 𝐴) = 𝐴 → 𝐴 = (𝐴 ∖ 𝐴))
16		difid 3902	. . . . 5 ⊢ (𝐴 ∖ 𝐴) = ∅
17	15, 16	syl6eq 2660	. . . 4 ⊢ ((V ∖ 𝐴) = 𝐴 → 𝐴 = ∅)
18	10, 17	eqtrd 2644	. . 3 ⊢ ((V ∖ 𝐴) = 𝐴 → V = ∅)
19	18	necon3i 2814	. 2 ⊢ (V ≠ ∅ → (V ∖ 𝐴) ≠ 𝐴)
20	1, 19	ax-mp 5	1 ⊢ (V ∖ 𝐴) ≠ 𝐴

Syntax hints:   = wceq 1475   ≠ wne 2780  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875

This theorem is referenced by: (None)