Theorem undif4 2321

Description: Distribute union over difference.

Assertion

Ref	Expression
undif4	⊢ ((A ∩ C) = ∅ → (A ∪ (B ∖ C)) = ((A ∪ B) ∖ C))

Proof of Theorem undif4

Step	Hyp	Ref	Expression
1		pm2.61 124	. . . . . . . 8 ⊢ ((x ∈ A → ¬ x ∈ C) → ((¬ x ∈ A → ¬ x ∈ C) → ¬ x ∈ C))
2		ax-1 4	. . . . . . . 8 ⊢ (¬ x ∈ C → (¬ x ∈ A → ¬ x ∈ C))
3	1, 2	impbid1 516	. . . . . . 7 ⊢ ((x ∈ A → ¬ x ∈ C) → ((¬ x ∈ A → ¬ x ∈ C) ↔ ¬ x ∈ C))
4		df-or 224	. . . . . . 7 ⊢ ((x ∈ A ⋁ ¬ x ∈ C) ↔ (¬ x ∈ A → ¬ x ∈ C))
5	3, 4	syl5bb 531	. . . . . 6 ⊢ ((x ∈ A → ¬ x ∈ C) → ((x ∈ A ⋁ ¬ x ∈ C) ↔ ¬ x ∈ C))
6	5	anbi2d 615	. . . . 5 ⊢ ((x ∈ A → ¬ x ∈ C) → (((x ∈ A ⋁ x ∈ B) ⋀ (x ∈ A ⋁ ¬ x ∈ C)) ↔ ((x ∈ A ⋁ x ∈ B) ⋀ ¬ x ∈ C)))
7		eldif 2053	. . . . . . 7 ⊢ (x ∈ (B ∖ C) ↔ (x ∈ B ⋀ ¬ x ∈ C))
8	7	orbi2i 255	. . . . . 6 ⊢ ((x ∈ A ⋁ x ∈ (B ∖ C)) ↔ (x ∈ A ⋁ (x ∈ B ⋀ ¬ x ∈ C)))
9		ordi 595	. . . . . 6 ⊢ ((x ∈ A ⋁ (x ∈ B ⋀ ¬ x ∈ C)) ↔ ((x ∈ A ⋁ x ∈ B) ⋀ (x ∈ A ⋁ ¬ x ∈ C)))
10	8, 9	bitr 173	. . . . 5 ⊢ ((x ∈ A ⋁ x ∈ (B ∖ C)) ↔ ((x ∈ A ⋁ x ∈ B) ⋀ (x ∈ A ⋁ ¬ x ∈ C)))
11		elun 2169	. . . . . 6 ⊢ (x ∈ (A ∪ B) ↔ (x ∈ A ⋁ x ∈ B))
12	11	anbi1i 481	. . . . 5 ⊢ ((x ∈ (A ∪ B) ⋀ ¬ x ∈ C) ↔ ((x ∈ A ⋁ x ∈ B) ⋀ ¬ x ∈ C))
13	6, 10, 12	3bitr4g 554	. . . 4 ⊢ ((x ∈ A → ¬ x ∈ C) → ((x ∈ A ⋁ x ∈ (B ∖ C)) ↔ (x ∈ (A ∪ B) ⋀ ¬ x ∈ C)))
14		elun 2169	. . . 4 ⊢ (x ∈ (A ∪ (B ∖ C)) ↔ (x ∈ A ⋁ x ∈ (B ∖ C)))
15		eldif 2053	. . . 4 ⊢ (x ∈ ((A ∪ B) ∖ C) ↔ (x ∈ (A ∪ B) ⋀ ¬ x ∈ C))
16	13, 14, 15	3bitr4g 554	. . 3 ⊢ ((x ∈ A → ¬ x ∈ C) → (x ∈ (A ∪ (B ∖ C)) ↔ x ∈ ((A ∪ B) ∖ C)))
17	16	19.20i 990	. 2 ⊢ (∀x(x ∈ A → ¬ x ∈ C) → ∀x(x ∈ (A ∪ (B ∖ C)) ↔ x ∈ ((A ∪ B) ∖ C)))
18		disj1 2308	. 2 ⊢ ((A ∩ C) = ∅ ↔ ∀x(x ∈ A → ¬ x ∈ C))
19		dfcleq 1468	. 2 ⊢ ((A ∪ (B ∖ C)) = ((A ∪ B) ∖ C) ↔ ∀x(x ∈ (A ∪ (B ∖ C)) ↔ x ∈ ((A ∪ B) ∖ C)))
20	17, 18, 19	3imtr4 219	1 ⊢ ((A ∩ C) = ∅ → (A ∪ (B ∖ C)) = ((A ∪ B) ∖ C))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956   ∖ cdif 2040   ∪ cun 2041   ∩ cin 2042  ∅c0 2276

This theorem is referenced by:  phplem1 4494

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ral 1646  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-nul 2277

Copyright terms: Public domain