![]() |
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.) |
Ref | Expression |
---|---|
pweq | ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3846 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵)) | |
2 | 1 | abbidv 2906 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑥 ∣ 𝑥 ⊆ 𝐵}) |
3 | df-pw 4381 | . 2 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} | |
4 | df-pw 4381 | . 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵} | |
5 | 2, 3, 4 | 3eqtr4g 2839 | 1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 {cab 2763 ⊆ wss 3792 𝒫 cpw 4379 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-in 3799 df-ss 3806 df-pw 4381 |
This theorem is referenced by: pweqi 4383 pweqd 4384 axpweq 5076 pwexg 5090 pwssun 5257 knatar 6879 pwdom 8400 canth2g 8402 pwfi 8549 fival 8606 marypha1lem 8627 marypha1 8628 wdompwdom 8772 canthwdom 8773 r1sucg 8929 ranklim 9004 r1pwALT 9006 isacn 9200 dfac12r 9303 dfac12k 9304 pwsdompw 9361 ackbij1lem8 9384 ackbij1lem14 9390 r1om 9401 fictb 9402 isfin1a 9449 isfin2 9451 isfin3 9453 isfin3ds 9486 isf33lem 9523 domtriomlem 9599 ttukeylem1 9666 elgch 9779 wunpw 9864 wunex2 9895 wuncval2 9904 eltskg 9907 eltsk2g 9908 tskpwss 9909 tskpw 9910 inar1 9932 grupw 9952 grothpw 9983 grothpwex 9984 axgroth6 9985 grothomex 9986 grothac 9987 axdc4uz 13102 hashpw 13537 hashbc 13551 ackbijnn 14964 incexclem 14972 rami 16123 ismre 16636 isacs 16697 isacs2 16699 acsfiel 16700 isacs1i 16703 mreacs 16704 isssc 16865 acsficl 17557 pmtrfval 18253 istopg 21107 istopon 21124 eltg 21169 tgdom 21190 ntrval 21248 nrmsep3 21567 iscmp 21600 cmpcov 21601 cmpsublem 21611 cmpsub 21612 tgcmp 21613 uncmp 21615 hauscmplem 21618 is1stc 21653 2ndc1stc 21663 llyi 21686 nllyi 21687 cldllycmp 21707 isfbas 22041 isfil 22059 filss 22065 fgval 22082 elfg 22083 isufil 22115 alexsublem 22256 alexsubb 22258 alexsubALTlem1 22259 alexsubALTlem2 22260 alexsubALTlem4 22262 alexsubALT 22263 restmetu 22783 bndth 23165 ovolicc2 23726 uhgreq12g 26413 uhgr0vb 26420 isupgr 26432 isumgr 26443 isuspgr 26501 isusgr 26502 isausgr 26513 lfuhgr1v0e 26601 usgrexmpl 26610 nbuhgr2vtx1edgblem 26698 ex-pw 27861 iscref 30509 indv 30672 sigaval 30771 issiga 30772 isrnsigaOLD 30773 isrnsiga 30774 issgon 30784 isldsys 30817 issros 30836 measval 30859 isrnmeas 30861 rankpwg 32865 neibastop1 32942 neibastop2lem 32943 neibastop2 32944 neibastop3 32945 neifg 32954 limsucncmpi 33027 bj-snglex 33533 bj-ismoore 33632 cover2g 34134 isnacs 38227 mrefg2 38230 aomclem8 38590 islssfg2 38600 lnr2i 38645 pwelg 38822 fsovd 39258 fsovcnvlem 39263 dssmapfvd 39267 clsk1independent 39300 ntrneibex 39327 stoweidlem50 41194 stoweidlem57 41201 issal 41458 omessle 41639 vsetrec 43554 elpglem3 43564 |
Copyright terms: Public domain | W3C validator |