| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ssequn2 | Structured version Visualization version GIF version | ||
| Description: A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.) |
| Ref | Expression |
|---|---|
| ssequn2 | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssequn1 4186 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) | |
| 2 | uncom 4158 | . . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) | |
| 3 | 2 | eqeq1i 2742 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) |
| 4 | 1, 3 | bitri 275 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 ∪ cun 3949 ⊆ wss 3951 |
| 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-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-ss 3968 |
| This theorem is referenced by: unabs 4265 undifr 4483 tppreqb 4805 pwssun 5575 cnvimassrndm 6172 relresfld 6296 ordssun 6486 ordequn 6487 onunel 6489 onun2 6492 oneluni 6503 fsnunf 7205 sorpssun 7750 ordunpr 7846 omun 7909 fodomr 9168 unfi 9211 enp1ilem 9312 pwfilem 9356 fodomfir 9368 brwdom2 9613 sucprcreg 9641 dfacfin7 10439 hashbclem 14491 incexclem 15872 ramub1lem1 17064 ramub1lem2 17065 mreexmrid 17686 lspun0 21009 lbsextlem4 21163 cldlp 23158 ordtuni 23198 lfinun 23533 cldsubg 24119 trust 24238 nulmbl2 25571 limcmpt2 25919 cnplimc 25922 dvreslem 25944 dvaddbr 25974 dvmulbr 25975 dvmulbrOLD 25976 lhop 26055 plypf1 26251 coeeulem 26263 coeeu 26264 coef2 26270 rlimcnp 27008 noetalem1 27786 addsproplem2 28003 ex-un 30443 shs0i 31468 chj0i 31474 disjun0 32608 ffsrn 32740 difioo 32784 symgcom2 33104 eulerpartlemt 34373 fineqvac 35111 subfacp1lem1 35184 cvmscld 35278 mthmpps 35587 refssfne 36359 topjoin 36366 pibt2 37418 poimirlem3 37630 poimirlem28 37655 rntrclfvOAI 42702 istopclsd 42711 nacsfix 42723 diophrw 42770 tfsconcatb0 43357 onsucunipr 43385 oaun3 43395 clcnvlem 43636 cnvrcl0 43638 dmtrcl 43640 rntrcl 43641 iunrelexp0 43715 dmtrclfvRP 43743 rntrclfv 43745 cotrclrcl 43755 clsk3nimkb 44053 limciccioolb 45636 limcicciooub 45652 ioccncflimc 45900 icocncflimc 45904 stoweidlem44 46059 dirkercncflem3 46120 fourierdlem62 46183 ismeannd 46482 cycl3grtri 47914 |
| Copyright terms: Public domain | W3C validator |