Proof of Theorem difininv
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | indif1 4282 | . . . . . 6
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | 
| 2 | 1 | eqeq1i 2742 | . . . . 5
⊢ (((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ↔ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ∅) | 
| 3 |  | ssdif0 4366 | . . . . 5
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐶 ↔ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ∅) | 
| 4 | 2, 3 | sylbb2 238 | . . . 4
⊢ (((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ → (𝐴 ∩ 𝐵) ⊆ 𝐶) | 
| 5 | 4 | adantr 480 | . . 3
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) ⊆ 𝐶) | 
| 6 |  | inss2 4238 | . . . 4
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | 
| 7 | 6 | a1i 11 | . . 3
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) ⊆ 𝐵) | 
| 8 | 5, 7 | ssind 4241 | . 2
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐵)) | 
| 9 |  | indif1 4282 | . . . . . 6
⊢ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∖ 𝐴) | 
| 10 | 9 | eqeq1i 2742 | . . . . 5
⊢ (((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅ ↔ ((𝐶 ∩ 𝐵) ∖ 𝐴) = ∅) | 
| 11 |  | ssdif0 4366 | . . . . 5
⊢ ((𝐶 ∩ 𝐵) ⊆ 𝐴 ↔ ((𝐶 ∩ 𝐵) ∖ 𝐴) = ∅) | 
| 12 | 10, 11 | sylbb2 238 | . . . 4
⊢ (((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅ → (𝐶 ∩ 𝐵) ⊆ 𝐴) | 
| 13 | 12 | adantl 481 | . . 3
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐶 ∩ 𝐵) ⊆ 𝐴) | 
| 14 |  | inss2 4238 | . . . 4
⊢ (𝐶 ∩ 𝐵) ⊆ 𝐵 | 
| 15 | 14 | a1i 11 | . . 3
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐶 ∩ 𝐵) ⊆ 𝐵) | 
| 16 | 13, 15 | ssind 4241 | . 2
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐶 ∩ 𝐵) ⊆ (𝐴 ∩ 𝐵)) | 
| 17 | 8, 16 | eqssd 4001 | 1
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = (𝐶 ∩ 𝐵)) |