| 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 4614 | . 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 𝒫 cpw 4600 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: undefval 8301 pmvalg 8877 marypha1lem 9473 marypha1 9474 r1val3 9878 ackbij2lem2 10279 ackbij2lem3 10280 r1om 10283 isfin2 10334 hsmexlem8 10464 vdwmc 17016 hashbcval 17040 ismre 17633 mrcfval 17651 mrisval 17673 mreexexlemd 17687 brssc 17858 lubfval 18395 glbfval 18408 isclat 18545 issubmgm 18715 issubm 18816 issubg 19144 cntzfval 19338 lsmfval 19656 lsmpropd 19695 pj1fval 19712 issubrng 20547 issubrg 20571 rgspnval 20612 lssset 20931 lspfval 20971 lsppropd 21017 islbs 21075 sraval 21174 ocvfval 21684 isobs 21740 islinds 21829 aspval 21893 opsrval 22064 ply1frcl 22322 evls1fval 22323 basis1 22957 baspartn 22961 cldval 23031 ntrfval 23032 clsfval 23033 mretopd 23100 neifval 23107 lpfval 23146 cncls2 23281 iscnrm 23331 iscnrm2 23346 2ndcsep 23467 kgenval 23543 xkoval 23595 dfac14 23626 qtopval 23703 qtopval2 23704 isfbas 23837 trfbas2 23851 flimval 23971 elflim 23979 flimclslem 23992 fclsfnflim 24035 fclscmp 24038 tsmsfbas 24136 tsmsval2 24138 ustval 24211 utopval 24241 mopnfss 24453 setsmstopn 24490 met2ndc 24536 madeval 27891 elmade2 27907 istrkgb 28463 isuhgr 29077 isushgr 29078 isuhgrop 29087 uhgrun 29091 uhgrstrrepe 29095 isupgr 29101 upgrop 29111 isumgr 29112 upgrun 29135 umgrun 29137 isuspgr 29169 isusgr 29170 isuspgrop 29178 isusgrop 29179 ausgrusgrb 29182 usgrstrrepe 29252 issubgr 29288 uhgrspansubgrlem 29307 usgrexi 29458 1hevtxdg1 29524 umgr2v2e 29543 zarcmplem 33880 ismeas 34200 omsval 34295 omscl 34297 omsf 34298 oms0 34299 carsgval 34305 omsmeas 34325 erdszelem3 35198 erdsze 35207 kur14 35221 iscvm 35264 mpstval 35540 mclsval 35568 bj-imdirvallem 37181 pibp21 37416 heibor 37828 idlval 38020 igenval 38068 paddfval 39799 pclfvalN 39891 polfvalN 39906 docaffvalN 41123 docafvalN 41124 djaffvalN 41135 djafvalN 41136 dochffval 41351 dochfval 41352 djhffval 41398 djhfval 41399 lpolsetN 41484 lcdlss2N 41622 mzpclval 42736 dfac21 43078 islmodfg 43081 islssfg 43082 rfovd 44014 fsovrfovd 44022 gneispace2 44145 ismnu 44280 sge0val 46381 ismea 46466 psmeasure 46486 caragenval 46508 isome 46509 omeunile 46520 isomennd 46546 ovnval 46556 hspmbl 46644 isvonmbl 46653 afv2eq12d 47227 isisubgr 47848 isubgruhgr 47854 stgrfv 47920 stgrusgra 47926 gpgov 48001 gpgusgra 48012 lincop 48325 lcoop 48328 islininds 48363 ldepsnlinc 48425 isclatd 48872 |
| Copyright terms: Public domain | W3C validator |