![]() |
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 4179 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) | |
2 | uncom 4152 | . . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) | |
3 | 2 | eqeq1i 2738 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) |
4 | 1, 3 | bitri 275 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1542 ∪ cun 3945 ⊆ wss 3947 |
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-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3952 df-in 3954 df-ss 3964 |
This theorem is referenced by: unabs 4253 undifr 4481 tppreqb 4807 pwssun 5570 cnvimassrndm 6148 relresfld 6272 ordssun 6463 ordequn 6464 onunel 6466 onun2 6469 oneluni 6480 fsnunf 7178 sorpssun 7715 ordunpr 7809 omun 7873 fodomr 9124 unfi 9168 pwfilem 9173 enp1ilem 9274 pwfilemOLD 9342 brwdom2 9564 sucprcreg 9592 dfacfin7 10390 hashbclem 14407 incexclem 15778 ramub1lem1 16955 ramub1lem2 16956 mreexmrid 17583 lspun0 20610 lbsextlem4 20762 cldlp 22636 ordtuni 22676 lfinun 23011 cldsubg 23597 trust 23716 nulmbl2 25035 limcmpt2 25383 cnplimc 25386 dvreslem 25408 dvaddbr 25437 dvmulbr 25438 lhop 25515 plypf1 25708 coeeulem 25720 coeeu 25721 coef2 25727 rlimcnp 26450 noetalem1 27224 addsproplem2 27434 ex-un 29657 shs0i 30680 chj0i 30686 disjun0 31804 ffsrn 31932 difioo 31971 symgcom2 32223 eulerpartlemt 33308 fineqvac 34035 subfacp1lem1 34108 cvmscld 34202 mthmpps 34511 gg-dvmulbr 35113 refssfne 35181 topjoin 35188 pibt2 36236 poimirlem3 36429 poimirlem28 36454 rntrclfvOAI 41362 istopclsd 41371 nacsfix 41383 diophrw 41430 tfsconcatb0 42027 onsucunipr 42055 oaun3 42065 clcnvlem 42307 cnvrcl0 42309 dmtrcl 42311 rntrcl 42312 iunrelexp0 42386 dmtrclfvRP 42414 rntrclfv 42416 cotrclrcl 42426 clsk3nimkb 42724 limciccioolb 44272 limcicciooub 44288 ioccncflimc 44536 icocncflimc 44540 stoweidlem44 44695 dirkercncflem3 44756 fourierdlem62 44819 ismeannd 45118 |
Copyright terms: Public domain | W3C validator |