Theorem compneOLD 39420

Description: Obsolete proof of compne 39419 as of 11-Nov-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
compneOLD	⊢ (V ∖ 𝐴) ≠ 𝐴

Proof of Theorem compneOLD

Step	Hyp	Ref	Expression
1		vn0 4126	. 2 ⊢ V ≠ ∅
2		ssun1 3975	. . . . . . . 8 ⊢ V ⊆ (V ∪ 𝐴)
3		ssv 3822	. . . . . . . 8 ⊢ (V ∪ 𝐴) ⊆ V
4	2, 3	eqssi 3815	. . . . . . 7 ⊢ V = (V ∪ 𝐴)
5		undif1 4238	. . . . . . 7 ⊢ ((V ∖ 𝐴) ∪ 𝐴) = (V ∪ 𝐴)
6	4, 5	eqtr4i 2825	. . . . . 6 ⊢ V = ((V ∖ 𝐴) ∪ 𝐴)
7		uneq1 3959	. . . . . 6 ⊢ ((V ∖ 𝐴) = 𝐴 → ((V ∖ 𝐴) ∪ 𝐴) = (𝐴 ∪ 𝐴))
8	6, 7	syl5eq 2846	. . . . 5 ⊢ ((V ∖ 𝐴) = 𝐴 → V = (𝐴 ∪ 𝐴))
9		unidm 3955	. . . . 5 ⊢ (𝐴 ∪ 𝐴) = 𝐴
10	8, 9	syl6eq 2850	. . . 4 ⊢ ((V ∖ 𝐴) = 𝐴 → V = 𝐴)
11		difabs 4093	. . . . . . 7 ⊢ ((V ∖ 𝐴) ∖ 𝐴) = (V ∖ 𝐴)
12		id 22	. . . . . . 7 ⊢ ((V ∖ 𝐴) = 𝐴 → (V ∖ 𝐴) = 𝐴)
13	11, 12	syl5req 2847	. . . . . 6 ⊢ ((V ∖ 𝐴) = 𝐴 → 𝐴 = ((V ∖ 𝐴) ∖ 𝐴))
14		difeq1 3920	. . . . . 6 ⊢ ((V ∖ 𝐴) = 𝐴 → ((V ∖ 𝐴) ∖ 𝐴) = (𝐴 ∖ 𝐴))
15	13, 14	eqtrd 2834	. . . . 5 ⊢ ((V ∖ 𝐴) = 𝐴 → 𝐴 = (𝐴 ∖ 𝐴))
16		difid 4150	. . . . 5 ⊢ (𝐴 ∖ 𝐴) = ∅
17	15, 16	syl6eq 2850	. . . 4 ⊢ ((V ∖ 𝐴) = 𝐴 → 𝐴 = ∅)
18	10, 17	eqtrd 2834	. . 3 ⊢ ((V ∖ 𝐴) = 𝐴 → V = ∅)
19	18	necon3i 3004	. 2 ⊢ (V ≠ ∅ → (V ∖ 𝐴) ≠ 𝐴)
20	1, 19	ax-mp 5	1 ⊢ (V ∖ 𝐴) ≠ 𝐴

Syntax hints:   = wceq 1653   ≠ wne 2972  Vcvv 3386   ∖ cdif 3767   ∪ cun 3768  ∅c0 4116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ne 2973  df-ral 3095  df-rab 3099  df-v 3388  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117

This theorem is referenced by: (None)