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 4518 | . . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) | |
2 | 1 | ralbii 3088 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
3 | dfss3 3888 | . 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵) | |
4 | unissb 4853 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | |
5 | 2, 3, 4 | 3bitr4i 306 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∈ wcel 2110 ∀wral 3061 ⊆ wss 3866 𝒫 cpw 4513 ∪ cuni 4819 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-11 2158 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-v 3410 df-in 3873 df-ss 3883 df-pw 4515 df-uni 4820 |
This theorem is referenced by: pwssb 5009 elpwpw 5010 elpwuni 5013 intss2 5016 rintn0 5017 dftr4 5166 uniixp 8602 fipwss 9045 dffi3 9047 uniwf 9435 numacn 9663 dfac12lem2 9758 fin23lem32 9958 isf34lem4 9991 isf34lem5 9992 fin1a2lem12 10025 itunitc1 10034 fpwwe2lem11 10255 tsksuc 10376 unirnioo 13037 restid 16938 mrcuni 17124 isacs3lem 18048 dmdprdd 19386 dprdfeq0 19409 dprdres 19415 dprdss 19416 dprdz 19417 subgdmdprd 19421 subgdprd 19422 dprd2dlem1 19428 dprd2da 19429 dmdprdsplit2lem 19432 ablfac1b 19457 lssintcl 20001 lbsextlem2 20196 lbsextlem3 20197 cssmre 20655 topgele 21827 topontopn 21837 unitg 21864 fctop 21901 cctop 21903 ppttop 21904 epttop 21906 mretopd 21989 resttopon 22058 ordtuni 22087 conncompcld 22331 islocfin 22414 kgentopon 22435 txuni2 22462 ptuni2 22473 ptbasfi 22478 xkouni 22496 prdstopn 22525 txdis 22529 txcmplem2 22539 xkococnlem 22556 qtoptop2 22596 qtopuni 22599 tgqtop 22609 opnfbas 22739 neifil 22777 filunibas 22778 trfil1 22783 flimfil 22866 cldsubg 23008 tgpconncompeqg 23009 tgpconncomp 23010 tsmsxplem1 23050 utoptop 23132 unirnblps 23317 unirnbl 23318 setsmstopn 23376 tngtopn 23548 bndth 23855 bcthlem5 24225 ovolficcss 24366 ovollb 24376 voliunlem2 24448 voliunlem3 24449 uniioovol 24476 uniioombl 24486 opnmbllem 24498 ubthlem1 28951 hsupcl 29420 hsupss 29422 hsupunss 29424 hsupval2 29490 fnpreimac 30728 unicls 31567 pwsiga 31810 sigainb 31816 insiga 31817 pwldsys 31837 ddemeas 31916 omssubadd 31979 cvmsss2 32949 dfon2lem2 33479 ntruni 34253 clsint2 34255 neibastop1 34285 neibastop2lem 34286 neibastop3 34288 topmeet 34290 topjoin 34291 fnemeet1 34292 fnemeet2 34293 fnejoin1 34294 opnmbllem0 35550 heiborlem1 35706 elrfi 40219 pwpwuni 42278 0ome 43742 |
Copyright terms: Public domain | W3C validator |