![]() |
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 3965 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-in 3422 df-ss 3429 df-pw 3964 |
This theorem is referenced by: undefval 7048 pmvalg 7508 marypha1lem 7972 marypha1 7973 r1val3 8334 ackbij1lem5 8679 ackbij2lem2 8695 ackbij2lem3 8696 r1om 8699 isfin2 8749 hsmexlem8 8879 vdwmc 14976 hashbcval 15002 ismre 15544 mrcfval 15562 mrisval 15584 mreexexlemd 15598 brssc 15767 lubfval 16272 glbfval 16285 isclat 16403 issubm 16642 issubg 16865 cntzfval 17022 symgval 17068 lsmfval 17338 lsmpropd 17375 pj1fval 17392 issubrg 18056 lssset 18205 lspfval 18244 lsppropd 18289 islbs 18347 sraval 18447 aspval 18600 opsrval 18746 ply1frcl 18955 evls1fval 18956 ocvfval 19277 isobs 19331 islinds 19415 basis1 20013 baspartn 20017 cldval 20086 ntrfval 20087 clsfval 20088 mretopd 20156 neifval 20163 lpfval 20202 cncls2 20337 iscnrm 20387 iscnrm2 20402 2ndcsep 20522 kgenval 20598 xkoval 20650 dfac14 20681 qtopval 20758 qtopval2 20759 isfbas 20892 trfbas2 20906 flimval 21026 elflim 21034 flimclslem 21047 fclsfnflim 21090 fclscmp 21093 tsmsfbas 21190 tsmsval2 21192 ustval 21265 utopval 21295 mopnfss 21506 setsmstopn 21541 met2ndc 21586 istrkgb 24551 isumgra 25090 isuslgra 25118 isusgra 25119 edgss 25127 ismeas 29069 omsval 29165 omscl 29167 omsf 29168 omsvalOLD 29169 omsclOLD 29171 omsfOLD 29172 oms0 29173 oms0OLD 29177 carsgval 29183 omsmeas 29203 omsmeasOLD 29204 erdszelem3 29964 erdsze 29973 kur14 29987 iscvm 30030 mpstval 30221 mclsval 30249 heibor 32197 idlval 32290 igenval 32338 paddfval 33406 pclfvalN 33498 polfvalN 33513 docaffvalN 34733 docafvalN 34734 djaffvalN 34745 djafvalN 34746 dochffval 34961 dochfval 34962 djhffval 35008 djhfval 35009 lpolsetN 35094 lcdlss2N 35232 mzpclval 35611 dfac21 35968 islmodfg 35971 islssfg 35972 rgspnval 36078 sge0val 38245 ismea 38326 psmeasure 38346 caragenval 38351 isome 38352 omeunile 38363 isomennd 38389 ovnval 38399 hspmbl 38488 isuhgr 39196 isushgr 39197 isuhgrop 39209 uhgrun 39213 isupgr 39222 isumgr 39231 upgrun 39253 umgrun 39255 isuspgr 39286 isusgr 39287 isusgrop 39296 ausgrusgrb 39299 issubgr 39392 uhgrspansubgrlem 39411 usgrexi 39555 umgr2v2e 39611 isuhgrALTV 39950 isushgrALTV 39951 uhgun 39964 issubmgm 40061 lincop 40473 lcoop 40476 islininds 40511 ldepsnlinc 40573 |
Copyright terms: Public domain | W3C validator |