![]() |
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 3774 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵)) | |
2 | 1 | abbidv 2889 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑥 ∣ 𝑥 ⊆ 𝐵}) |
3 | df-pw 4297 | . 2 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} | |
4 | df-pw 4297 | . 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵} | |
5 | 2, 3, 4 | 3eqtr4g 2829 | 1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1630 {cab 2756 ⊆ wss 3721 𝒫 cpw 4295 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-in 3728 df-ss 3735 df-pw 4297 |
This theorem is referenced by: pweqi 4299 pweqd 4300 axpweq 4970 pwex 4976 pwexg 4978 pwssun 5153 knatar 6749 pwdom 8267 canth2g 8269 pwfi 8416 fival 8473 marypha1lem 8494 marypha1 8495 wdompwdom 8638 canthwdom 8639 r1sucg 8795 ranklim 8870 r1pwALT 8872 isacn 9066 dfac12r 9169 dfac12k 9170 pwsdompw 9227 ackbij1lem8 9250 ackbij1lem14 9256 r1om 9267 fictb 9268 isfin1a 9315 isfin2 9317 isfin3 9319 isfin3ds 9352 isf33lem 9389 domtriomlem 9465 ttukeylem1 9532 elgch 9645 wunpw 9730 wunex2 9761 wuncval2 9770 eltskg 9773 eltsk2g 9774 tskpwss 9775 tskpw 9776 inar1 9798 grupw 9818 grothpw 9849 grothpwex 9850 axgroth6 9851 grothomex 9852 grothac 9853 axdc4uz 12990 hashpw 13424 hashbc 13438 ackbijnn 14766 incexclem 14774 rami 15925 ismre 16457 isacs 16518 isacs2 16520 acsfiel 16521 isacs1i 16524 mreacs 16525 isssc 16686 acsficl 17378 pmtrfval 18076 istopg 20919 istopon 20936 eltg 20981 tgdom 21002 ntrval 21060 nrmsep3 21379 iscmp 21411 cmpcov 21412 cmpsublem 21422 cmpsub 21423 tgcmp 21424 uncmp 21426 hauscmplem 21429 is1stc 21464 2ndc1stc 21474 llyi 21497 nllyi 21498 cldllycmp 21518 isfbas 21852 isfil 21870 filss 21876 fgval 21893 elfg 21894 isufil 21926 alexsublem 22067 alexsubb 22069 alexsubALTlem1 22070 alexsubALTlem2 22071 alexsubALTlem4 22073 alexsubALT 22074 restmetu 22594 bndth 22976 ovolicc2 23509 uhgreq12g 26180 uhgr0vb 26187 isupgr 26199 isumgr 26210 isuspgr 26268 isusgr 26269 isausgr 26280 lfuhgr1v0e 26368 usgrexmpl 26377 nbuhgr2vtx1edgblem 26469 ex-pw 27622 iscref 30245 indv 30408 sigaval 30507 issiga 30508 isrnsigaOLD 30509 isrnsiga 30510 issgon 30520 isldsys 30553 issros 30572 measval 30595 isrnmeas 30597 rankpwg 32607 neibastop1 32685 neibastop2lem 32686 neibastop2 32687 neibastop3 32688 neifg 32697 limsucncmpi 32775 bj-snglex 33286 bj-ismoore 33384 cover2g 33834 isnacs 37786 mrefg2 37789 aomclem8 38150 islssfg2 38160 lnr2i 38205 pwelg 38384 fsovd 38821 fsovcnvlem 38826 dssmapfvd 38830 clsk1independent 38863 ntrneibex 38890 stoweidlem50 40778 stoweidlem57 40785 issal 41045 omessle 41226 vsetrec 42967 elpglem3 42977 |
Copyright terms: Public domain | W3C validator |