Theorem undifdc 6560

Description: Union of complementary parts into whole. This is a case where we can strengthen undifss 3344 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.)

Assertion

Ref	Expression
undifdc	⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑦,𝐵

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem undifdc

Dummy variables 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 19	. . . 4 ⊢ (𝑤 = ∅ → 𝑤 = ∅)
2		difeq2 3096	. . . 4 ⊢ (𝑤 = ∅ → (𝐴 ∖ 𝑤) = (𝐴 ∖ ∅))
3	1, 2	uneq12d 3139	. . 3 ⊢ (𝑤 = ∅ → (𝑤 ∪ (𝐴 ∖ 𝑤)) = (∅ ∪ (𝐴 ∖ ∅)))
4	3	eqeq2d 2094	. 2 ⊢ (𝑤 = ∅ → (𝐴 = (𝑤 ∪ (𝐴 ∖ 𝑤)) ↔ 𝐴 = (∅ ∪ (𝐴 ∖ ∅))))
5		id 19	. . . 4 ⊢ (𝑤 = 𝑣 → 𝑤 = 𝑣)
6		difeq2 3096	. . . 4 ⊢ (𝑤 = 𝑣 → (𝐴 ∖ 𝑤) = (𝐴 ∖ 𝑣))
7	5, 6	uneq12d 3139	. . 3 ⊢ (𝑤 = 𝑣 → (𝑤 ∪ (𝐴 ∖ 𝑤)) = (𝑣 ∪ (𝐴 ∖ 𝑣)))
8	7	eqeq2d 2094	. 2 ⊢ (𝑤 = 𝑣 → (𝐴 = (𝑤 ∪ (𝐴 ∖ 𝑤)) ↔ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))))
9		id 19	. . . 4 ⊢ (𝑤 = (𝑣 ∪ {𝑧}) → 𝑤 = (𝑣 ∪ {𝑧}))
10		difeq2 3096	. . . 4 ⊢ (𝑤 = (𝑣 ∪ {𝑧}) → (𝐴 ∖ 𝑤) = (𝐴 ∖ (𝑣 ∪ {𝑧})))
11	9, 10	uneq12d 3139	. . 3 ⊢ (𝑤 = (𝑣 ∪ {𝑧}) → (𝑤 ∪ (𝐴 ∖ 𝑤)) = ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))))
12	11	eqeq2d 2094	. 2 ⊢ (𝑤 = (𝑣 ∪ {𝑧}) → (𝐴 = (𝑤 ∪ (𝐴 ∖ 𝑤)) ↔ 𝐴 = ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧})))))
13		id 19	. . . 4 ⊢ (𝑤 = 𝐵 → 𝑤 = 𝐵)
14		difeq2 3096	. . . 4 ⊢ (𝑤 = 𝐵 → (𝐴 ∖ 𝑤) = (𝐴 ∖ 𝐵))
15	13, 14	uneq12d 3139	. . 3 ⊢ (𝑤 = 𝐵 → (𝑤 ∪ (𝐴 ∖ 𝑤)) = (𝐵 ∪ (𝐴 ∖ 𝐵)))
16	15	eqeq2d 2094	. 2 ⊢ (𝑤 = 𝐵 → (𝐴 = (𝑤 ∪ (𝐴 ∖ 𝑤)) ↔ 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵))))
17		un0 3299	. . . 4 ⊢ ((𝐴 ∖ ∅) ∪ ∅) = (𝐴 ∖ ∅)
18		uncom 3128	. . . 4 ⊢ ((𝐴 ∖ ∅) ∪ ∅) = (∅ ∪ (𝐴 ∖ ∅))
19		dif0 3335	. . . 4 ⊢ (𝐴 ∖ ∅) = 𝐴
20	17, 18, 19	3eqtr3ri 2112	. . 3 ⊢ 𝐴 = (∅ ∪ (𝐴 ∖ ∅))
21	20	a1i 9	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (∅ ∪ (𝐴 ∖ ∅)))
22		difundi 3234	. . . . . . 7 ⊢ (𝐴 ∖ (𝑣 ∪ {𝑧})) = ((𝐴 ∖ 𝑣) ∩ (𝐴 ∖ {𝑧}))
23	22	uneq2i 3135	. . . . . 6 ⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))) = ((𝑣 ∪ {𝑧}) ∪ ((𝐴 ∖ 𝑣) ∩ (𝐴 ∖ {𝑧})))
24		undi 3230	. . . . . 6 ⊢ ((𝑣 ∪ {𝑧}) ∪ ((𝐴 ∖ 𝑣) ∩ (𝐴 ∖ {𝑧}))) = (((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) ∩ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧})))
25	23, 24	eqtri 2103	. . . . 5 ⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))) = (((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) ∩ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧})))
26		simp3 941	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐴)
27	26	ad3antrrr 476	. . . . . . . . . . 11 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝐵 ⊆ 𝐴)
28		simplrr 503	. . . . . . . . . . . 12 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑧 ∈ (𝐵 ∖ 𝑣))
29	28	eldifad 2995	. . . . . . . . . . 11 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑧 ∈ 𝐵)
30	27, 29	sseldd 3011	. . . . . . . . . 10 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑧 ∈ 𝐴)
31	30	snssd 3556	. . . . . . . . 9 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → {𝑧} ⊆ 𝐴)
32		ssequn1 3154	. . . . . . . . 9 ⊢ ({𝑧} ⊆ 𝐴 ↔ ({𝑧} ∪ 𝐴) = 𝐴)
33	31, 32	sylib 120	. . . . . . . 8 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ({𝑧} ∪ 𝐴) = 𝐴)
34		simpr 108	. . . . . . . . 9 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣)))
35	34	uneq2d 3138	. . . . . . . 8 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ({𝑧} ∪ 𝐴) = ({𝑧} ∪ (𝑣 ∪ (𝐴 ∖ 𝑣))))
36	33, 35	eqtr3d 2117	. . . . . . 7 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝐴 = ({𝑧} ∪ (𝑣 ∪ (𝐴 ∖ 𝑣))))
37		uncom 3128	. . . . . . . . 9 ⊢ (𝑣 ∪ {𝑧}) = ({𝑧} ∪ 𝑣)
38	37	uneq1i 3134	. . . . . . . 8 ⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) = (({𝑧} ∪ 𝑣) ∪ (𝐴 ∖ 𝑣))
39		unass 3141	. . . . . . . 8 ⊢ (({𝑧} ∪ 𝑣) ∪ (𝐴 ∖ 𝑣)) = ({𝑧} ∪ (𝑣 ∪ (𝐴 ∖ 𝑣)))
40	38, 39	eqtri 2103	. . . . . . 7 ⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) = ({𝑧} ∪ (𝑣 ∪ (𝐴 ∖ 𝑣)))
41	36, 40	syl6reqr 2134	. . . . . 6 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) = 𝐴)
42		unass 3141	. . . . . . . 8 ⊢ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧})) = (𝑣 ∪ ({𝑧} ∪ (𝐴 ∖ {𝑧})))
43		uncom 3128	. . . . . . . . . 10 ⊢ ({𝑧} ∪ (𝐴 ∖ {𝑧})) = ((𝐴 ∖ {𝑧}) ∪ {𝑧})
44		simp1 939	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
45	44	ad3antrrr 476	. . . . . . . . . . 11 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
46		dcdifsnid 6194	. . . . . . . . . . 11 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝑧 ∈ 𝐴) → ((𝐴 ∖ {𝑧}) ∪ {𝑧}) = 𝐴)
47	45, 30, 46	syl2anc 403	. . . . . . . . . 10 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝐴 ∖ {𝑧}) ∪ {𝑧}) = 𝐴)
48	43, 47	syl5eq 2127	. . . . . . . . 9 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ({𝑧} ∪ (𝐴 ∖ {𝑧})) = 𝐴)
49	48	uneq2d 3138	. . . . . . . 8 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → (𝑣 ∪ ({𝑧} ∪ (𝐴 ∖ {𝑧}))) = (𝑣 ∪ 𝐴))
50	42, 49	syl5eq 2127	. . . . . . 7 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧})) = (𝑣 ∪ 𝐴))
51		simplrl 502	. . . . . . . . 9 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑣 ⊆ 𝐵)
52	51, 27	sstrd 3020	. . . . . . . 8 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝑣 ⊆ 𝐴)
53		ssequn1 3154	. . . . . . . 8 ⊢ (𝑣 ⊆ 𝐴 ↔ (𝑣 ∪ 𝐴) = 𝐴)
54	52, 53	sylib 120	. . . . . . 7 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → (𝑣 ∪ 𝐴) = 𝐴)
55	50, 54	eqtrd 2115	. . . . . 6 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧})) = 𝐴)
56	41, 55	ineq12d 3186	. . . . 5 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → (((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ 𝑣)) ∩ ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ {𝑧}))) = (𝐴 ∩ 𝐴))
57	25, 56	syl5eq 2127	. . . 4 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))) = (𝐴 ∩ 𝐴))
58		inidm 3193	. . . 4 ⊢ (𝐴 ∩ 𝐴) = 𝐴
59	57, 58	syl6req 2132	. . 3 ⊢ (((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) ∧ 𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣))) → 𝐴 = ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧}))))
60	59	ex 113	. 2 ⊢ ((((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) ∧ 𝑣 ∈ Fin) ∧ (𝑣 ⊆ 𝐵 ∧ 𝑧 ∈ (𝐵 ∖ 𝑣))) → (𝐴 = (𝑣 ∪ (𝐴 ∖ 𝑣)) → 𝐴 = ((𝑣 ∪ {𝑧}) ∪ (𝐴 ∖ (𝑣 ∪ {𝑧})))))
61		simp2 940	. 2 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
62	4, 8, 12, 16, 21, 60, 61	findcard2sd 6537	1 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))

Syntax hints:   → wi 4   ∧ wa 102  DECID wdc 776   ∧ w3a 920   = wceq 1285   ∈ wcel 1434  ∀wral 2353   ∖ cdif 2981   ∪ cun 2982   ∩ cin 2983   ⊆ wss 2984  ∅c0 3269  {csn 3422  Fincfn 6386

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3919  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-setind 4315  ax-iinf 4365

This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-if 3374  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-tr 3902  df-id 4083  df-iord 4156  df-on 4158  df-suc 4161  df-iom 4368  df-xp 4406  df-rel 4407  df-cnv 4408  df-co 4409  df-dm 4410  df-rn 4411  df-res 4412  df-ima 4413  df-iota 4933  df-fun 4970  df-fn 4971  df-f 4972  df-f1 4973  df-fo 4974  df-f1o 4975  df-fv 4976  df-er 6221  df-en 6387  df-fin 6389

This theorem is referenced by:  undiffi  6561