| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pweq | Structured version Visualization version GIF version | ||
| Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.) |
| Ref | Expression |
|---|---|
| pweq | ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqimss 4042 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
| 2 | 1 | sspwd 4613 | . 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
| 3 | eqimss2 4043 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴) | |
| 4 | 3 | sspwd 4613 | . 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴) |
| 5 | 2, 4 | eqssd 4001 | 1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 𝒫 cpw 4600 |
| 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-v 3482 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: pweqi 4616 pweqd 4617 axpweq 5351 pwexg 5378 pwssun 5575 knatar 7377 pwdom 9169 canth2g 9171 pwfi 9357 fival 9452 marypha1lem 9473 marypha1 9474 wdompwdom 9618 canthwdom 9619 r1sucg 9809 ranklim 9884 r1pwALT 9886 isacn 10084 dfac12r 10187 dfac12k 10188 pwsdompw 10243 ackbij1lem8 10266 ackbij1lem14 10272 r1om 10283 fictb 10284 isfin1a 10332 isfin2 10334 isfin3 10336 isfin3ds 10369 isf33lem 10406 domtriomlem 10482 ttukeylem1 10549 elgch 10662 wunpw 10747 wunex2 10778 wuncval2 10787 eltskg 10790 eltsk2g 10791 tskpwss 10792 tskpw 10793 inar1 10815 grupw 10835 grothpw 10866 grothpwex 10867 axgroth6 10868 grothomex 10869 grothac 10870 axdc4uz 14025 hashpw 14475 hashbc 14492 ackbijnn 15864 incexclem 15872 rami 17053 ismre 17633 isacs 17694 isacs2 17696 acsfiel 17697 isacs1i 17700 mreacs 17701 isssc 17864 acsficl 18592 efmnd 18883 pmtrfval 19468 selvffval 22137 istopg 22901 istopon 22918 eltg 22964 tgdom 22985 ntrval 23044 nrmsep3 23363 iscmp 23396 cmpcov 23397 cmpsublem 23407 cmpsub 23408 tgcmp 23409 uncmp 23411 hauscmplem 23414 is1stc 23449 2ndc1stc 23459 llyi 23482 nllyi 23483 cldllycmp 23503 isfbas 23837 isfil 23855 filss 23861 fgval 23878 elfg 23879 isufil 23911 alexsublem 24052 alexsubb 24054 alexsubALTlem1 24055 alexsubALTlem2 24056 alexsubALTlem4 24058 alexsubALT 24059 restmetu 24583 bndth 24990 ovolicc2 25557 uhgreq12g 29082 uhgr0vb 29089 isupgr 29101 isumgr 29112 isuspgr 29169 isusgr 29170 isausgr 29181 lfuhgr1v0e 29271 nbuhgr2vtx1edgblem 29368 ex-pw 30448 indv 32837 iscref 33843 sigaval 34112 issiga 34113 isrnsiga 34114 issgon 34124 isldsys 34157 issros 34176 measval 34199 isrnmeas 34201 rankpwg 36170 neibastop1 36360 neibastop2lem 36361 neibastop2 36362 neibastop3 36363 neifg 36372 limsucncmpi 36446 bj-snglex 36974 bj-ismoore 37106 pibp19 37415 pibt2 37418 cover2g 37723 isnacs 42715 mrefg2 42718 aomclem8 43073 islssfg2 43083 lnr2i 43128 pwelg 43573 fsovd 44021 fsovcnvlem 44026 dssmapfvd 44030 clsk1independent 44059 ntrneibex 44086 mnuop123d 44281 stoweidlem50 46065 stoweidlem57 46072 issal 46329 omessle 46513 grtri 47907 vsetrec 49222 elpglem3 49232 pgindnf 49235 |
| Copyright terms: Public domain | W3C validator |