| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > indif2 | Structured version Visualization version GIF version | ||
| Description: Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.) |
| Ref | Expression |
|---|---|
| indif2 | ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inass 4228 | . 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) | |
| 2 | invdif 4279 | . 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | |
| 3 | invdif 4279 | . . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶) | |
| 4 | 3 | ineq2i 4217 | . 2 ⊢ (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵 ∖ 𝐶)) |
| 5 | 1, 2, 4 | 3eqtr3ri 2774 | 1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 Vcvv 3480 ∖ cdif 3948 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-in 3958 |
| This theorem is referenced by: indif1 4282 indifcom 4283 rabdif 4321 frpoind 6363 wfiOLD 6372 marypha1lem 9473 frind 9790 difopn 23042 restcld 23180 difmbl 25578 voliunlem1 25585 difuncomp 32566 imadifxp 32614 difelcarsg 34312 carsgclctunlem1 34319 topbnd 36325 bj-disj2r 37029 nlpineqsn 37409 mblfinlem3 37666 mblfinlem4 37667 gneispace 44147 saldifcl2 46343 caragenuncllem 46527 carageniuncllem1 46536 iscnrm3rlem1 48837 |
| Copyright terms: Public domain | W3C validator |