![]() |
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 4146 | . 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) | |
2 | invdif 4195 | . 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | |
3 | invdif 4195 | . . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶) | |
4 | 3 | ineq2i 4136 | . 2 ⊢ (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵 ∖ 𝐶)) |
5 | 1, 2, 4 | 3eqtr3ri 2830 | 1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 Vcvv 3441 ∖ cdif 3878 ∩ cin 3880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-dif 3884 df-in 3888 |
This theorem is referenced by: indif1 4198 indifcom 4199 wfi 6149 marypha1lem 8881 difopn 21639 restcld 21777 difmbl 24147 voliunlem1 24154 difuncomp 30317 imadifxp 30364 difelcarsg 31678 carsgclctunlem1 31685 frpoind 33193 frind 33198 topbnd 33785 bj-disj2r 34464 nlpineqsn 34825 mblfinlem3 35096 mblfinlem4 35097 rabdif 39399 gneispace 40837 saldifcl2 42968 caragenuncllem 43151 carageniuncllem1 43160 |
Copyright terms: Public domain | W3C validator |