![]() |
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 | selpw 4198 | . . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) | |
2 | 1 | ralbii 3009 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
3 | dfss3 3625 | . 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵) | |
4 | unissb 4501 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | |
5 | 2, 3, 4 | 3bitr4i 292 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∈ wcel 2030 ∀wral 2941 ⊆ wss 3607 𝒫 cpw 4191 ∪ cuni 4468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-v 3233 df-in 3614 df-ss 3621 df-pw 4193 df-uni 4469 |
This theorem is referenced by: pwssb 4644 elpwpw 4645 elpwuni 4648 rintn0 4651 dftr4 4790 uniixp 7973 fipwss 8376 dffi3 8378 uniwf 8720 numacn 8910 dfac12lem2 9004 fin23lem32 9204 isf34lem4 9237 isf34lem5 9238 fin1a2lem12 9271 itunitc1 9280 fpwwe2lem12 9501 tsksuc 9622 unirnioo 12311 restid 16141 mrcuni 16328 isacs3lem 17213 dmdprdd 18444 dprdfeq0 18467 dprdres 18473 dprdss 18474 dprdz 18475 subgdmdprd 18479 subgdprd 18480 dprd2dlem1 18486 dprd2da 18487 dmdprdsplit2lem 18490 ablfac1b 18515 lssintcl 19012 lbsextlem2 19207 lbsextlem3 19208 cssmre 20085 topgele 20782 topontopn 20792 unitg 20819 fctop 20856 cctop 20858 ppttop 20859 epttop 20861 mretopd 20944 toponmre 20945 resttopon 21013 ordtuni 21042 conncompcld 21285 islocfin 21368 kgentopon 21389 txuni2 21416 ptuni2 21427 ptbasfi 21432 xkouni 21450 prdstopn 21479 txdis 21483 txcmplem2 21493 xkococnlem 21510 qtoptop2 21550 qtopuni 21553 tgqtop 21563 opnfbas 21693 neifil 21731 filunibas 21732 trfil1 21737 flimfil 21820 cldsubg 21961 tgpconncompeqg 21962 tgpconncomp 21963 tsmsxplem1 22003 utoptop 22085 unirnblps 22271 unirnbl 22272 setsmstopn 22330 tngtopn 22501 bndth 22804 bcthlem5 23171 ovolficcss 23284 ovollb 23293 voliunlem2 23365 voliunlem3 23366 uniioovol 23393 uniioombl 23403 opnmbllem 23415 ubthlem1 27854 hsupcl 28326 hsupss 28328 hsupunss 28330 hsupval2 28396 unicls 30077 pwsiga 30321 sigainb 30327 insiga 30328 ddemeas 30427 omssubadd 30490 cvmsss2 31382 dfon2lem2 31813 ntruni 32447 clsint2 32449 neibastop1 32479 neibastop2lem 32480 neibastop3 32482 topmeet 32484 topjoin 32485 fnemeet1 32486 fnemeet2 32487 fnejoin1 32488 bj-intss 33178 opnmbllem0 33575 heiborlem1 33740 elrfi 37574 pwpwuni 39539 0ome 41064 |
Copyright terms: Public domain | W3C validator |