![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > undif | Structured version Visualization version GIF version |
Description: Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.) |
Ref | Expression |
---|---|
undif | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssequn1 3926 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) | |
2 | undif2 4188 | . . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) | |
3 | 2 | eqeq1i 2765 | . 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
4 | 1, 3 | bitr4i 267 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1632 ∖ cdif 3712 ∪ cun 3713 ⊆ wss 3715 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 |
This theorem is referenced by: raldifeq 4203 difsnid 4486 fveqf1o 6721 ralxpmap 8075 undifixp 8112 dfdom2 8149 sbthlem5 8241 sbthlem6 8242 domunsn 8277 fodomr 8278 mapdom2 8298 limensuci 8303 findcard2 8367 unfi 8394 marypha1lem 8506 brwdom2 8645 infdifsn 8729 ackbij1lem12 9265 ackbij1lem18 9271 ssfin4 9344 fin23lem28 9374 fin23lem30 9376 fin1a2lem13 9446 canthp1lem1 9686 xrsupss 12352 xrinfmss 12353 hashssdif 13412 hashfun 13436 hashf1lem2 13452 fsumless 14747 incexclem 14787 incexc 14788 fprodsplit1f 14940 pwssplit1 19281 frlmsslss2 20336 mdetdiaglem 20626 mdetrlin 20630 mdetrsca 20631 mdetralt 20636 smadiadet 20698 isclo 21113 cmpcld 21427 rrxcph 23400 rrxdstprj1 23412 uniiccmbl 23578 itgss3 23800 dchreq 25203 axlowdimlem7 26048 axlowdimlem10 26051 padct 29827 resf1o 29835 fprodeq02 29899 locfinref 30238 indval2 30406 esummono 30446 gsumesum 30451 sigaclfu2 30514 measxun2 30603 measvuni 30607 measssd 30608 pmeasmono 30716 eulerpartlemt 30763 tgoldbachgtde 31068 noextendseq 32147 poimirlem9 33749 poimirlem15 33755 poimirlem25 33765 diophrw 37842 eldioph2lem1 37843 eldioph2lem2 37844 kelac1 38153 fsumsplit1 40325 ioccncflimc 40619 icocncflimc 40623 dirkercncflem2 40842 dirkercncflem3 40843 sge0ss 41150 meassle 41201 meadif 41217 meaiininclem 41224 isomenndlem 41268 hspmbllem1 41364 hspmbllem2 41365 ovolval4lem1 41387 fsumsplitsndif 41871 |
Copyright terms: Public domain | W3C validator |