![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pweqd | Structured version Visualization version GIF version |
Description: Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
Ref | Expression |
---|---|
pweqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
pweqd | ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | pweq 4616 | . 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 𝒫 cpw 4602 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3955 df-ss 3965 df-pw 4604 |
This theorem is referenced by: undefval 8258 pmvalg 8828 marypha1lem 9425 marypha1 9426 r1val3 9830 ackbij2lem2 10232 ackbij2lem3 10233 r1om 10236 isfin2 10286 hsmexlem8 10416 vdwmc 16908 hashbcval 16932 ismre 17531 mrcfval 17549 mrisval 17571 mreexexlemd 17585 brssc 17758 lubfval 18300 glbfval 18313 isclat 18450 issubm 18681 issubg 19001 cntzfval 19179 lsmfval 19501 lsmpropd 19540 pj1fval 19557 issubrg 20356 lssset 20537 lspfval 20577 lsppropd 20622 islbs 20680 sraval 20782 ocvfval 21211 isobs 21267 islinds 21356 aspval 21419 opsrval 21593 ply1frcl 21829 evls1fval 21830 basis1 22445 baspartn 22449 cldval 22519 ntrfval 22520 clsfval 22521 mretopd 22588 neifval 22595 lpfval 22634 cncls2 22769 iscnrm 22819 iscnrm2 22834 2ndcsep 22955 kgenval 23031 xkoval 23083 dfac14 23114 qtopval 23191 qtopval2 23192 isfbas 23325 trfbas2 23339 flimval 23459 elflim 23467 flimclslem 23480 fclsfnflim 23523 fclscmp 23526 tsmsfbas 23624 tsmsval2 23626 ustval 23699 utopval 23729 mopnfss 23941 setsmstopn 23978 met2ndc 24024 madeval 27337 elmade2 27353 istrkgb 27696 isuhgr 28310 isushgr 28311 isuhgrop 28320 uhgrun 28324 uhgrstrrepe 28328 isupgr 28334 upgrop 28344 isumgr 28345 upgrun 28368 umgrun 28370 isuspgr 28402 isusgr 28403 isuspgrop 28411 isusgrop 28412 ausgrusgrb 28415 usgrstrrepe 28482 issubgr 28518 uhgrspansubgrlem 28537 usgrexi 28688 1hevtxdg1 28753 umgr2v2e 28772 zarcmplem 32850 ismeas 33186 omsval 33281 omscl 33283 omsf 33284 oms0 33285 carsgval 33291 omsmeas 33311 erdszelem3 34173 erdsze 34182 kur14 34196 iscvm 34239 mpstval 34515 mclsval 34543 bj-imdirvallem 36050 pibp21 36285 heibor 36678 idlval 36870 igenval 36918 paddfval 38657 pclfvalN 38749 polfvalN 38764 docaffvalN 39981 docafvalN 39982 djaffvalN 39993 djafvalN 39994 dochffval 40209 dochfval 40210 djhffval 40256 djhfval 40257 lpolsetN 40342 lcdlss2N 40480 mzpclval 41449 dfac21 41794 islmodfg 41797 islssfg 41798 rgspnval 41896 rfovd 42738 fsovrfovd 42746 gneispace2 42869 ismnu 43006 sge0val 45069 ismea 45154 psmeasure 45174 caragenval 45196 isome 45197 omeunile 45208 isomennd 45234 ovnval 45244 hspmbl 45332 isvonmbl 45341 afv2eq12d 45910 issubmgm 46546 issubrng 46711 lincop 47043 lcoop 47046 islininds 47081 ldepsnlinc 47143 isclatd 47562 |
Copyright terms: Public domain | W3C validator |