| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > disjdifr | Structured version Visualization version GIF version | ||
| Description: A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.) |
| Ref | Expression |
|---|---|
| disjdifr | ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | incom 4209 | . 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∩ 𝐴) | |
| 2 | disjdif 4472 | . 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | |
| 3 | 1, 2 | eqtr3i 2767 | 1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∖ cdif 3948 ∩ cin 3950 ∅c0 4333 |
| 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-fal 1553 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 df-ss 3968 df-nul 4334 |
| This theorem is referenced by: ssdifin0 4486 fvsnun1 7202 fveqf1o 7322 f1ofvswap 7326 ralxpmap 8936 difsnen 9093 domunsn 9167 limensuci 9193 pssnn 9208 marypha1lem 9473 dif1card 10050 ackbij1lem18 10276 canthp1lem1 10692 grothprim 10874 hashgval 14372 hashun3 14423 hashfun 14476 hashbclem 14491 setsfun 17208 setsfun0 17209 setsid 17244 mreexexlem4d 17690 pwssplit1 21058 islindf4 21858 psdmul 22170 neitr 23188 regsep2 23384 restmetu 24583 volinun 25581 tdeglem4 26099 noetasuplem3 27780 noetasuplem4 27781 difeq 32537 disjdifprg 32588 tocycfvres1 33130 tocycfvres2 33131 cycpmfvlem 33132 cycpmfv3 33135 cycpmcl 33136 rprmdvdsprod 33562 measunl 34217 eulerpartlemt 34373 mthmpps 35587 cldbnd 36327 poimirlem15 37642 poimirlem16 37643 poimirlem19 37646 poimirlem27 37654 selvvvval 42595 evlselvlem 42596 evlselv 42597 eldioph2lem1 42771 eldioph2lem2 42772 diophren 42824 kelac1 43075 isomenndlem 46545 seposep 48823 |
| Copyright terms: Public domain | W3C validator |