This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem undif4

Description: Distribute union over difference. (Contributed by NM, 17-May-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion undif4 ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 pm2.621 ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐶 ) → ¬ 𝑥 ∈ 𝐶 ) )
2 olc ⊢ ( ¬ 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐶 ) )
3 1 2 impbid1 ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐶 ) ↔ ¬ 𝑥 ∈ 𝐶 ) )
4 3 anbi2d ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) → ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
5 eldif ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) )
6 5 orbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
7 ordi ⊢ ( ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐶 ) ) )
8 6 7 bitri ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐶 ) ) )
9 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
10 9 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) )
11 4 8 10 3bitr4g ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
12 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) )
13 eldif ⊢ ( 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝐶 ) )
14 11 12 13 3bitr4g ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐶 ) ) )
15 14 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) → ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐶 ) ) )
16 disj1 ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐶 ) )
17 dfcleq ⊢ ( ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐶 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐶 ) ) )
18 15 16 17 3imtr4i ⊢ ( ( 𝐴 ∩ 𝐶 ) = ∅ → ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐶 ) )