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 4538 | . 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 𝒫 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: undefval 7931 pmvalg 8406 marypha1lem 8885 marypha1 8886 r1val3 9255 ackbij2lem2 9650 ackbij2lem3 9651 r1om 9654 isfin2 9704 hsmexlem8 9834 vdwmc 16302 hashbcval 16326 ismre 16849 mrcfval 16867 mrisval 16889 mreexexlemd 16903 brssc 17072 lubfval 17576 glbfval 17589 isclat 17707 issubm 17956 issubg 18217 cntzfval 18388 symgval 18435 lsmfval 18692 lsmpropd 18732 pj1fval 18749 issubrg 19464 lssset 19634 lspfval 19674 lsppropd 19719 islbs 19777 sraval 19877 aspval 20030 opsrval 20183 ply1frcl 20409 evls1fval 20410 ocvfval 20738 isobs 20792 islinds 20881 basis1 21486 baspartn 21490 cldval 21559 ntrfval 21560 clsfval 21561 mretopd 21628 neifval 21635 lpfval 21674 cncls2 21809 iscnrm 21859 iscnrm2 21874 2ndcsep 21995 kgenval 22071 xkoval 22123 dfac14 22154 qtopval 22231 qtopval2 22232 isfbas 22365 trfbas2 22379 flimval 22499 elflim 22507 flimclslem 22520 fclsfnflim 22563 fclscmp 22566 tsmsfbas 22663 tsmsval2 22665 ustval 22738 utopval 22768 mopnfss 22980 setsmstopn 23015 met2ndc 23060 istrkgb 26168 isuhgr 26772 isushgr 26773 isuhgrop 26782 uhgrun 26786 uhgrstrrepe 26790 isupgr 26796 upgrop 26806 isumgr 26807 upgrun 26830 umgrun 26832 isuspgr 26864 isusgr 26865 isuspgrop 26873 isusgrop 26874 ausgrusgrb 26877 usgrstrrepe 26944 issubgr 26980 uhgrspansubgrlem 26999 usgrexi 27150 1hevtxdg1 27215 umgr2v2e 27234 ismeas 31357 omsval 31450 omscl 31452 omsf 31453 oms0 31454 carsgval 31460 omsmeas 31480 erdszelem3 32337 erdsze 32346 kur14 32360 iscvm 32403 mpstval 32679 mclsval 32707 madeval 33186 bj-imdirval 34364 pibp21 34578 heibor 34980 idlval 35172 igenval 35220 paddfval 36813 pclfvalN 36905 polfvalN 36920 docaffvalN 38137 docafvalN 38138 djaffvalN 38149 djafvalN 38150 dochffval 38365 dochfval 38366 djhffval 38412 djhfval 38413 lpolsetN 38498 lcdlss2N 38636 mzpclval 39200 dfac21 39544 islmodfg 39547 islssfg 39548 rgspnval 39646 rfovd 40225 fsovrfovd 40233 gneispace2 40360 ismnu 40474 sge0val 42525 ismea 42610 psmeasure 42630 caragenval 42652 isome 42653 omeunile 42664 isomennd 42690 ovnval 42700 hspmbl 42788 isvonmbl 42797 afv2eq12d 43291 issubmgm 43933 lincop 44391 lcoop 44394 islininds 44429 ldepsnlinc 44491 |
Copyright terms: Public domain | W3C validator |