![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sspwuni | Structured version Visualization version GIF version |
Description: Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
Ref | Expression |
---|---|
sspwuni | ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | velpw 4611 | . . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) | |
2 | 1 | ralbii 3082 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
3 | dfss3 3967 | . 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵) | |
4 | unissb 4946 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | |
5 | 2, 3, 4 | 3bitr4i 302 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2098 ∀wral 3050 ⊆ wss 3946 𝒫 cpw 4606 ∪ cuni 4912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-v 3463 df-ss 3963 df-pw 4608 df-uni 4913 |
This theorem is referenced by: pwssb 5108 elpwpw 5109 elpwuni 5112 intss2 5115 rintn0 5116 dftr4 5276 uniixp 8949 fipwss 9468 dffi3 9470 uniwf 9858 numacn 10088 dfac12lem2 10183 fin23lem32 10383 isf34lem4 10416 isf34lem5 10417 fin1a2lem12 10450 itunitc1 10459 fpwwe2lem11 10680 tsksuc 10801 unirnioo 13475 restid 17443 mrcuni 17629 isacs3lem 18562 dmdprdd 19994 dprdfeq0 20017 dprdres 20023 dprdss 20024 dprdz 20025 subgdmdprd 20029 subgdprd 20030 dprd2dlem1 20036 dprd2da 20037 dmdprdsplit2lem 20040 ablfac1b 20065 lssintcl 20888 lbsextlem2 21087 lbsextlem3 21088 cssmre 21681 topgele 22915 topontopn 22925 unitg 22953 fctop 22990 cctop 22992 ppttop 22993 epttop 22995 mretopd 23079 resttopon 23148 ordtuni 23177 conncompcld 23421 islocfin 23504 kgentopon 23525 txuni2 23552 ptuni2 23563 ptbasfi 23568 xkouni 23586 prdstopn 23615 txdis 23619 txcmplem2 23629 xkococnlem 23646 qtoptop2 23686 qtopuni 23689 tgqtop 23699 opnfbas 23829 neifil 23867 filunibas 23868 trfil1 23873 flimfil 23956 cldsubg 24098 tgpconncompeqg 24099 tgpconncomp 24100 tsmsxplem1 24140 utoptop 24222 unirnblps 24408 unirnbl 24409 setsmstopn 24469 tngtopn 24650 bndth 24967 bcthlem5 25339 ovolficcss 25481 ovollb 25491 voliunlem2 25563 voliunlem3 25564 uniioovol 25591 uniioombl 25601 opnmbllem 25613 ubthlem1 30795 hsupcl 31264 hsupss 31266 hsupunss 31268 hsupval2 31334 fnpreimac 32579 unicls 33674 pwsiga 33919 sigainb 33925 insiga 33926 pwldsys 33946 ddemeas 34025 omssubadd 34090 cvmsss2 35054 dfon2lem2 35556 ntruni 35987 clsint2 35989 neibastop1 36019 neibastop2lem 36020 neibastop3 36022 topmeet 36024 topjoin 36025 fnemeet1 36026 fnemeet2 36027 fnejoin1 36028 opnmbllem0 37305 heiborlem1 37460 elrfi 42288 pwpwuni 44595 0ome 46087 |
Copyright terms: Public domain | W3C validator |