![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pweqi | Structured version Visualization version GIF version |
Description: Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
Ref | Expression |
---|---|
pweqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
pweqi | ⊢ 𝒫 𝐴 = 𝒫 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | pweq 4353 | . 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝒫 𝐴 = 𝒫 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 𝒫 cpw 4350 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2778 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2787 df-cleq 2793 df-clel 2796 df-in 3777 df-ss 3784 df-pw 4352 |
This theorem is referenced by: pwfi 8504 rankxplim 8993 pwcda1 9305 fin23lem17 9449 mnfnre 10372 qtopres 21829 hmphdis 21927 ust0 22350 umgrpredgv 26375 issubgr 26504 uhgrissubgr 26508 cusgredg 26673 cffldtocusgr 26696 konigsbergiedgw 27594 shsspwh 28627 circtopn 30419 rankeq1o 32790 onsucsuccmpi 32949 elrfi 38038 islmodfg 38419 clsk1indlem4 39119 clsk1indlem1 39120 clsk1independent 39121 omef 41451 caragensplit 41455 caragenelss 41456 carageneld 41457 omeunile 41460 caragensspw 41464 0ome 41484 isomennd 41486 ovn02 41523 lcoop 42994 lincvalsc0 43004 linc0scn0 43006 lincdifsn 43007 linc1 43008 lspsslco 43020 lincresunit3lem2 43063 lincresunit3 43064 |
Copyright terms: Public domain | W3C validator |