Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pweqd | Structured version Visualization version Unicode 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 4161 | . 2 | |
3 | 1, 2 | syl 17 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cpw 4158 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-in 3581 df-ss 3588 df-pw 4160 |
This theorem is referenced by: undefval 7402 pmvalg 7868 marypha1lem 8339 marypha1 8340 r1val3 8701 ackbij1lem5 9046 ackbij2lem2 9062 ackbij2lem3 9063 r1om 9066 isfin2 9116 hsmexlem8 9246 vdwmc 15682 hashbcval 15706 ismre 16250 mrcfval 16268 mrisval 16290 mreexexlemd 16304 brssc 16474 lubfval 16978 glbfval 16991 isclat 17109 issubm 17347 issubg 17594 cntzfval 17753 symgval 17799 lsmfval 18053 lsmpropd 18090 pj1fval 18107 issubrg 18780 lssset 18934 lspfval 18973 lsppropd 19018 islbs 19076 sraval 19176 aspval 19328 opsrval 19474 ply1frcl 19683 evls1fval 19684 ocvfval 20010 isobs 20064 islinds 20148 basis1 20754 baspartn 20758 cldval 20827 ntrfval 20828 clsfval 20829 mretopd 20896 neifval 20903 lpfval 20942 cncls2 21077 iscnrm 21127 iscnrm2 21142 2ndcsep 21262 kgenval 21338 xkoval 21390 dfac14 21421 qtopval 21498 qtopval2 21499 isfbas 21633 trfbas2 21647 flimval 21767 elflim 21775 flimclslem 21788 fclsfnflim 21831 fclscmp 21834 tsmsfbas 21931 tsmsval2 21933 ustval 22006 utopval 22036 mopnfss 22248 setsmstopn 22283 met2ndc 22328 istrkgb 25354 isuhgr 25955 isushgr 25956 isuhgrop 25965 uhgrun 25969 uhgrstrrepe 25973 isupgr 25979 upgrop 25989 isumgr 25990 upgrun 26013 umgrun 26015 isuspgr 26047 isusgr 26048 isuspgrop 26056 isusgrop 26057 ausgrusgrb 26060 usgrstrrepe 26127 issubgr 26163 uhgrspansubgrlem 26182 usgrexi 26337 1hevtxdg1 26402 umgr2v2e 26421 ismeas 30262 omsval 30355 omscl 30357 omsf 30358 oms0 30359 carsgval 30365 omsmeas 30385 erdszelem3 31175 erdsze 31184 kur14 31198 iscvm 31241 mpstval 31432 mclsval 31460 madeval 31935 heibor 33620 idlval 33812 igenval 33860 paddfval 35083 pclfvalN 35175 polfvalN 35190 docaffvalN 36410 docafvalN 36411 djaffvalN 36422 djafvalN 36423 dochffval 36638 dochfval 36639 djhffval 36685 djhfval 36686 lpolsetN 36771 lcdlss2N 36909 mzpclval 37288 dfac21 37636 islmodfg 37639 islssfg 37640 rgspnval 37738 rfovd 38295 fsovrfovd 38303 gneispace2 38430 sge0val 40583 ismea 40668 psmeasure 40688 caragenval 40707 isome 40708 omeunile 40719 isomennd 40745 ovnval 40755 hspmbl 40843 isvonmbl 40852 issubmgm 41789 lincop 42197 lcoop 42200 islininds 42235 ldepsnlinc 42297 |
Copyright terms: Public domain | W3C validator |