| 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 4605 | . . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) | |
| 2 | 1 | ralbii 3093 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
| 3 | dfss3 3972 | . 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵) | |
| 4 | unissb 4939 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∈ wcel 2108 ∀wral 3061 ⊆ wss 3951 𝒫 cpw 4600 ∪ cuni 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-v 3482 df-ss 3968 df-pw 4602 df-uni 4908 |
| This theorem is referenced by: pwssb 5101 elpwpw 5102 elpwuni 5105 intss2 5108 rintn0 5109 dftr4 5266 uniixp 8961 fipwss 9469 dffi3 9471 uniwf 9859 numacn 10089 dfac12lem2 10185 fin23lem32 10384 isf34lem4 10417 isf34lem5 10418 fin1a2lem12 10451 itunitc1 10460 fpwwe2lem11 10681 tsksuc 10802 unirnioo 13489 restid 17478 mrcuni 17664 isacs3lem 18587 dmdprdd 20019 dprdfeq0 20042 dprdres 20048 dprdss 20049 dprdz 20050 subgdmdprd 20054 subgdprd 20055 dprd2dlem1 20061 dprd2da 20062 dmdprdsplit2lem 20065 ablfac1b 20090 lssintcl 20962 lbsextlem2 21161 lbsextlem3 21162 cssmre 21711 topgele 22936 topontopn 22946 unitg 22974 fctop 23011 cctop 23013 ppttop 23014 epttop 23016 mretopd 23100 resttopon 23169 ordtuni 23198 conncompcld 23442 islocfin 23525 kgentopon 23546 txuni2 23573 ptuni2 23584 ptbasfi 23589 xkouni 23607 prdstopn 23636 txdis 23640 txcmplem2 23650 xkococnlem 23667 qtoptop2 23707 qtopuni 23710 tgqtop 23720 opnfbas 23850 neifil 23888 filunibas 23889 trfil1 23894 flimfil 23977 cldsubg 24119 tgpconncompeqg 24120 tgpconncomp 24121 tsmsxplem1 24161 utoptop 24243 unirnblps 24429 unirnbl 24430 setsmstopn 24490 tngtopn 24671 bndth 24990 bcthlem5 25362 ovolficcss 25504 ovollb 25514 voliunlem2 25586 voliunlem3 25587 uniioovol 25614 uniioombl 25624 opnmbllem 25636 ubthlem1 30889 hsupcl 31358 hsupss 31360 hsupunss 31362 hsupval2 31428 fnpreimac 32681 unicls 33902 pwsiga 34131 sigainb 34137 insiga 34138 pwldsys 34158 ddemeas 34237 omssubadd 34302 cvmsss2 35279 dfon2lem2 35785 ntruni 36328 clsint2 36330 neibastop1 36360 neibastop2lem 36361 neibastop3 36363 topmeet 36365 topjoin 36366 fnemeet1 36367 fnemeet2 36368 fnejoin1 36369 opnmbllem0 37663 heiborlem1 37818 elrfi 42705 pwpwuni 45062 0ome 46544 |
| Copyright terms: Public domain | W3C validator |