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 4545 | . . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) | |
2 | 1 | ralbii 3165 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
3 | dfss3 3955 | . 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵) | |
4 | unissb 4863 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | |
5 | 2, 3, 4 | 3bitr4i 304 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∈ wcel 2105 ∀wral 3138 ⊆ wss 3935 𝒫 cpw 4537 ∪ cuni 4832 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-v 3497 df-in 3942 df-ss 3951 df-pw 4539 df-uni 4833 |
This theorem is referenced by: pwssb 5015 elpwpw 5016 elpwuni 5019 rintn0 5022 dftr4 5169 uniixp 8474 fipwss 8882 dffi3 8884 uniwf 9237 numacn 9464 dfac12lem2 9559 fin23lem32 9755 isf34lem4 9788 isf34lem5 9789 fin1a2lem12 9822 itunitc1 9831 fpwwe2lem12 10052 tsksuc 10173 unirnioo 12827 restid 16697 mrcuni 16882 isacs3lem 17766 dmdprdd 19052 dprdfeq0 19075 dprdres 19081 dprdss 19082 dprdz 19083 subgdmdprd 19087 subgdprd 19088 dprd2dlem1 19094 dprd2da 19095 dmdprdsplit2lem 19098 ablfac1b 19123 lssintcl 19667 lbsextlem2 19862 lbsextlem3 19863 cssmre 20767 topgele 21468 topontopn 21478 unitg 21505 fctop 21542 cctop 21544 ppttop 21545 epttop 21547 mretopd 21630 resttopon 21699 ordtuni 21728 conncompcld 21972 islocfin 22055 kgentopon 22076 txuni2 22103 ptuni2 22114 ptbasfi 22119 xkouni 22137 prdstopn 22166 txdis 22170 txcmplem2 22180 xkococnlem 22197 qtoptop2 22237 qtopuni 22240 tgqtop 22250 opnfbas 22380 neifil 22418 filunibas 22419 trfil1 22424 flimfil 22507 cldsubg 22648 tgpconncompeqg 22649 tgpconncomp 22650 tsmsxplem1 22690 utoptop 22772 unirnblps 22958 unirnbl 22959 setsmstopn 23017 tngtopn 23188 bndth 23491 bcthlem5 23860 ovolficcss 23999 ovollb 24009 voliunlem2 24081 voliunlem3 24082 uniioovol 24109 uniioombl 24119 opnmbllem 24131 ubthlem1 28575 hsupcl 29044 hsupss 29046 hsupunss 29048 hsupval2 29114 fnpreimac 30345 unicls 31046 pwsiga 31289 sigainb 31295 insiga 31296 ddemeas 31395 omssubadd 31458 cvmsss2 32419 dfon2lem2 32927 ntruni 33573 clsint2 33575 neibastop1 33605 neibastop2lem 33606 neibastop3 33608 topmeet 33610 topjoin 33611 fnemeet1 33612 fnemeet2 33613 fnejoin1 33614 bj-intss 34286 opnmbllem0 34810 heiborlem1 34972 elrfi 39171 pwpwuni 41199 0ome 42692 |
Copyright terms: Public domain | W3C validator |