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 3745 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) | |
2 | uncom 3719 | . . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) | |
3 | 2 | eqeq1i 2615 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) |
4 | 1, 3 | bitri 263 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ∪ cun 3538 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-in 3547 df-ss 3554 |
This theorem is referenced by: unabs 3816 tppreqb 4277 pwssun 4944 pwundif 4945 relresfld 5579 ordssun 5744 ordequn 5745 oneluni 5757 fsnunf 6356 sorpssun 6842 ordunpr 6918 fodomr 7996 enp1ilem 8079 pwfilem 8143 brwdom2 8361 sucprcreg 8389 dfacfin7 9104 hashbclem 13093 incexclem 14407 ramub1lem1 15568 ramub1lem2 15569 mreexmrid 16126 lspun0 18832 lbsextlem4 18982 cldlp 20764 ordtuni 20804 lfinun 21138 cldsubg 21724 trust 21843 nulmbl2 23111 limcmpt2 23454 cnplimc 23457 dvreslem 23479 dvaddbr 23507 dvmulbr 23508 lhop 23583 plypf1 23772 coeeulem 23784 coeeu 23785 coef2 23791 rlimcnp 24492 ex-un 26673 shs0i 27692 chj0i 27698 disjun0 28790 ffsrn 28892 difioo 28934 eulerpartlemt 29760 subfacp1lem1 30415 cvmscld 30509 mthmpps 30733 refssfne 31523 topjoin 31530 poimirlem3 32582 poimirlem28 32607 rntrclfvOAI 36272 istopclsd 36281 nacsfix 36293 diophrw 36340 clcnvlem 36949 cnvrcl0 36951 dmtrcl 36953 rntrcl 36954 iunrelexp0 37013 dmtrclfvRP 37041 rntrclfv 37043 cotrclrcl 37053 clsk3nimkb 37358 limciccioolb 38688 limcicciooub 38704 ioccncflimc 38771 icocncflimc 38775 stoweidlem44 38937 dirkercncflem3 38998 fourierdlem62 39061 ismeannd 39360 |
Copyright terms: Public domain | W3C validator |