![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sspwb | Structured version Visualization version Unicode version |
Description: Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
Ref | Expression |
---|---|
sspwb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3407 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 32 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 3016 |
. . . . 5
![]() ![]() ![]() ![]() | |
4 | 3 | elpw 3925 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3 | elpw 3925 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 4, 5 | 3imtr4g 278 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | ssrdv 3406 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | ssel 3394 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | snex 4614 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 9 | elpw 3925 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 3 | snss 4065 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 10, 11 | bitr4i 260 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 9 | elpw 3925 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 3 | snss 4065 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 13, 14 | bitr4i 260 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 8, 12, 15 | 3imtr3g 277 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16 | ssrdv 3406 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 7, 17 | impbii 192 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-sep 4497 ax-nul 4506 ax-pr 4612 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-v 3015 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-pw 3921 df-sn 3937 df-pr 3939 |
This theorem is referenced by: pwel 4625 ssextss 4627 pweqb 4630 pwdom 7711 marypha1lem 7934 wdompwdom 8080 r1pwss 8242 pwwf 8265 rankpwi 8281 rankxplim 8337 ackbij2lem1 8636 fictb 8662 ssfin2 8737 ssfin3ds 8747 ttukeylem2 8927 hashbclem 12610 wrdexg 12677 incexclem 13905 hashbcss 14967 isacs1i 15574 mreacs 15575 acsfn 15576 sscpwex 15731 wunfunc 15815 isacs3lem 16423 isacs5lem 16426 tgcmp 20427 imastopn 20746 fgabs 20905 fgtr 20916 trfg 20917 ssufl 20944 alexsubb 21072 tsmsres 21169 cfiluweak 21321 cfilresi 22276 cmetss 22295 minveclem4a 22383 minveclem4 22385 minveclem4aOLD 22395 minveclem4OLD 22397 vitali 22583 sqff1o 24121 elsigagen2 28977 ldsysgenld 28989 ldgenpisyslem1 28992 measres 29051 imambfm 29090 ballotlem2 29327 neibastop1 31021 neibastop2lem 31022 neibastop2 31023 sstotbnd2 32108 isnacs3 35554 aomclem2 35915 sge0less 38293 sge0iunmptlemre 38316 |
Copyright terms: Public domain | W3C validator |