![]() |
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 4200 | . 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∩ 𝐴) | |
2 | disjdif 4470 | . 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | |
3 | 1, 2 | eqtr3i 2763 | 1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∖ cdif 3944 ∩ cin 3946 ∅c0 4321 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3950 df-in 3954 df-ss 3964 df-nul 4322 |
This theorem is referenced by: ssdifin0 4484 fvsnun1 7175 fveqf1o 7296 f1ofvswap 7299 ralxpmap 8886 difsnen 9049 domunsn 9123 limensuci 9149 pssnn 9164 marypha1lem 9424 dif1card 10001 ackbij1lem18 10228 canthp1lem1 10643 grothprim 10825 hashgval 14289 hashun3 14340 hashfun 14393 hashbclem 14407 setsfun 17100 setsfun0 17101 setsid 17137 mreexexlem4d 17587 pwssplit1 20658 islindf4 21377 neitr 22666 regsep2 22862 restmetu 24061 volinun 25045 tdeglem4 25559 noetasuplem3 27218 noetasuplem4 27219 difeq 31734 disjdifprg 31784 tocycfvres1 32247 tocycfvres2 32248 cycpmfvlem 32249 cycpmfv3 32252 cycpmcl 32253 measunl 33152 eulerpartlemt 33308 mthmpps 34511 cldbnd 35149 poimirlem15 36441 poimirlem16 36442 poimirlem19 36445 poimirlem27 36453 selvvvval 41107 evlselvlem 41108 evlselv 41109 eldioph2lem1 41431 eldioph2lem2 41432 diophren 41484 kelac1 41738 isomenndlem 45181 seposep 47460 |
Copyright terms: Public domain | W3C validator |