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 3990 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵)) | |
2 | 1 | abbidv 2882 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑥 ∣ 𝑥 ⊆ 𝐵}) |
3 | df-pw 4537 | . 2 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} | |
4 | df-pw 4537 | . 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵} | |
5 | 2, 3, 4 | 3eqtr4g 2878 | 1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 {cab 2796 ⊆ wss 3933 𝒫 cpw 4535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 df-pw 4537 |
This theorem is referenced by: pweqi 4539 pweqd 4540 axpweq 5256 pwexg 5270 pwssun 5448 knatar 7099 pwdom 8657 canth2g 8659 pwfi 8807 fival 8864 marypha1lem 8885 marypha1 8886 wdompwdom 9030 canthwdom 9031 r1sucg 9186 ranklim 9261 r1pwALT 9263 isacn 9458 dfac12r 9560 dfac12k 9561 pwsdompw 9614 ackbij1lem8 9637 ackbij1lem14 9643 r1om 9654 fictb 9655 isfin1a 9702 isfin2 9704 isfin3 9706 isfin3ds 9739 isf33lem 9776 domtriomlem 9852 ttukeylem1 9919 elgch 10032 wunpw 10117 wunex2 10148 wuncval2 10157 eltskg 10160 eltsk2g 10161 tskpwss 10162 tskpw 10163 inar1 10185 grupw 10205 grothpw 10236 grothpwex 10237 axgroth6 10238 grothomex 10239 grothac 10240 axdc4uz 13340 hashpw 13785 hashbc 13799 ackbijnn 15171 incexclem 15179 rami 16339 ismre 16849 isacs 16910 isacs2 16912 acsfiel 16913 isacs1i 16916 mreacs 16917 isssc 17078 acsficl 17769 pmtrfval 18507 selvffval 20257 istopg 21431 istopon 21448 eltg 21493 tgdom 21514 ntrval 21572 nrmsep3 21891 iscmp 21924 cmpcov 21925 cmpsublem 21935 cmpsub 21936 tgcmp 21937 uncmp 21939 hauscmplem 21942 is1stc 21977 2ndc1stc 21987 llyi 22010 nllyi 22011 cldllycmp 22031 isfbas 22365 isfil 22383 filss 22389 fgval 22406 elfg 22407 isufil 22439 alexsublem 22580 alexsubb 22582 alexsubALTlem1 22583 alexsubALTlem2 22584 alexsubALTlem4 22586 alexsubALT 22587 restmetu 23107 bndth 23489 ovolicc2 24050 uhgreq12g 26777 uhgr0vb 26784 isupgr 26796 isumgr 26807 isuspgr 26864 isusgr 26865 isausgr 26876 lfuhgr1v0e 26963 usgrexmpl 26972 nbuhgr2vtx1edgblem 27060 ex-pw 28135 iscref 31007 indv 31170 sigaval 31269 issiga 31270 isrnsiga 31271 issgon 31281 isldsys 31314 issros 31333 measval 31356 isrnmeas 31358 rankpwg 33527 neibastop1 33604 neibastop2lem 33605 neibastop2 33606 neibastop3 33607 neifg 33616 limsucncmpi 33690 bj-snglex 34182 bj-ismoore 34291 pibp19 34577 pibt2 34580 cover2g 34871 isnacs 39179 mrefg2 39182 aomclem8 39539 islssfg2 39549 lnr2i 39594 pwelg 39797 fsovd 40232 fsovcnvlem 40237 dssmapfvd 40241 clsk1independent 40274 ntrneibex 40301 mnuop123d 40475 stoweidlem50 42212 stoweidlem57 42219 issal 42476 omessle 42657 efmnd 43969 vsetrec 44733 elpglem3 44743 |
Copyright terms: Public domain | W3C validator |