![]() |
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 4040 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | 1 | sspwd 4619 | . 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
3 | eqimss2 4041 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴) | |
4 | 3 | sspwd 4619 | . 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴) |
5 | 2, 4 | eqssd 3999 | 1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 𝒫 cpw 4606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3475 df-in 3956 df-ss 3966 df-pw 4608 |
This theorem is referenced by: pweqi 4622 pweqd 4623 axpweq 5354 pwexg 5382 pwssun 5577 knatar 7371 pwdom 9160 canth2g 9162 pwfi 9209 pwfiOLD 9379 fival 9443 marypha1lem 9464 marypha1 9465 wdompwdom 9609 canthwdom 9610 r1sucg 9800 ranklim 9875 r1pwALT 9877 isacn 10075 dfac12r 10177 dfac12k 10178 pwsdompw 10235 ackbij1lem8 10258 ackbij1lem14 10264 r1om 10275 fictb 10276 isfin1a 10323 isfin2 10325 isfin3 10327 isfin3ds 10360 isf33lem 10397 domtriomlem 10473 ttukeylem1 10540 elgch 10653 wunpw 10738 wunex2 10769 wuncval2 10778 eltskg 10781 eltsk2g 10782 tskpwss 10783 tskpw 10784 inar1 10806 grupw 10826 grothpw 10857 grothpwex 10858 axgroth6 10859 grothomex 10860 grothac 10861 axdc4uz 13989 hashpw 14435 hashbc 14452 ackbijnn 15814 incexclem 15822 rami 16991 ismre 17577 isacs 17638 isacs2 17640 acsfiel 17641 isacs1i 17644 mreacs 17645 isssc 17810 acsficl 18546 efmnd 18829 pmtrfval 19412 selvffval 22066 istopg 22817 istopon 22834 eltg 22880 tgdom 22901 ntrval 22960 nrmsep3 23279 iscmp 23312 cmpcov 23313 cmpsublem 23323 cmpsub 23324 tgcmp 23325 uncmp 23327 hauscmplem 23330 is1stc 23365 2ndc1stc 23375 llyi 23398 nllyi 23399 cldllycmp 23419 isfbas 23753 isfil 23771 filss 23777 fgval 23794 elfg 23795 isufil 23827 alexsublem 23968 alexsubb 23970 alexsubALTlem1 23971 alexsubALTlem2 23972 alexsubALTlem4 23974 alexsubALT 23975 restmetu 24499 bndth 24904 ovolicc2 25471 uhgreq12g 28898 uhgr0vb 28905 isupgr 28917 isumgr 28928 isuspgr 28985 isusgr 28986 isausgr 28997 lfuhgr1v0e 29087 usgrexmpl 29096 nbuhgr2vtx1edgblem 29184 ex-pw 30259 iscref 33478 indv 33664 sigaval 33763 issiga 33764 isrnsiga 33765 issgon 33775 isldsys 33808 issros 33827 measval 33850 isrnmeas 33852 rankpwg 35798 neibastop1 35876 neibastop2lem 35877 neibastop2 35878 neibastop3 35879 neifg 35888 limsucncmpi 35962 bj-snglex 36485 bj-ismoore 36617 pibp19 36926 pibt2 36929 cover2g 37222 isnacs 42155 mrefg2 42158 aomclem8 42516 islssfg2 42526 lnr2i 42571 pwelg 43021 fsovd 43469 fsovcnvlem 43474 dssmapfvd 43478 clsk1independent 43507 ntrneibex 43534 mnuop123d 43730 stoweidlem50 45467 stoweidlem57 45474 issal 45731 omessle 45915 vsetrec 48212 elpglem3 48222 pgindnf 48225 |
Copyright terms: Public domain | W3C validator |