![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pweq | Structured version Visualization version Unicode version |
Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
pweq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3466 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | abbidv 2580 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-pw 3965 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-pw 3965 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3eqtr4g 2521 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-in 3423 df-ss 3430 df-pw 3965 |
This theorem is referenced by: pweqi 3967 pweqd 3968 axpweq 4597 pwex 4603 pwexg 4604 pwssun 4762 knatar 6278 pwdom 7755 canth2g 7757 pwfi 7900 fival 7957 marypha1lem 7978 marypha1 7979 wdompwdom 8124 canthwdom 8125 r1sucg 8271 ranklim 8346 r1pwALT 8348 isacn 8506 dfac12r 8607 dfac12k 8608 pwsdompw 8665 ackbij1lem5 8685 ackbij1lem8 8688 ackbij1lem14 8694 r1om 8705 fictb 8706 isfin1a 8753 isfin2 8755 isfin3 8757 isfin3ds 8790 isf33lem 8827 domtriomlem 8903 ttukeylem1 8970 elgch 9078 wunpw 9163 wunex2 9194 wuncval2 9203 eltskg 9206 eltsk2g 9207 tskpwss 9208 tskpw 9209 inar1 9231 grupw 9251 grothpw 9282 grothpwex 9283 axgroth6 9284 grothomex 9285 grothac 9286 axdc4uz 12234 hashpw 12647 hashbc 12655 ackbijnn 13941 incexclem 13949 rami 15027 ismre 15551 isacs 15612 isacs2 15614 acsfiel 15615 isacs1i 15618 mreacs 15619 isssc 15780 acsficl 16472 pmtrfval 17146 istopg 19980 istopon 19995 eltg 20027 tgdom 20049 ntrval 20106 nrmsep3 20426 iscmp 20458 cmpcov 20459 cmpsublem 20469 cmpsub 20470 tgcmp 20471 uncmp 20473 hauscmplem 20476 is1stc 20511 2ndc1stc 20521 llyi 20544 nllyi 20545 cldllycmp 20565 isfbas 20899 isfil 20917 filss 20923 fgval 20940 elfg 20941 isufil 20973 alexsublem 21114 alexsubb 21116 alexsubALTlem1 21117 alexsubALTlem2 21118 alexsubALTlem4 21120 alexsubALT 21121 restmetu 21640 bndth 22041 ovolicc2 22531 isuhgra 25081 isushgra 25084 uhgrac 25088 uhgraeq12d 25090 isausgra 25137 usgraeq12d 25145 ex-pw 25935 issubgo 26087 iscref 28722 indv 28885 sigaval 28983 issiga 28984 isrnsigaOLD 28985 isrnsiga 28986 issgon 28996 isldsys 29029 issros 29048 measval 29071 isrnmeas 29073 rankpwg 30986 neibastop1 31065 neibastop2lem 31066 neibastop2 31067 neibastop3 31068 neifg 31077 limsucncmpi 31155 bj-snglex 31613 cover2g 32087 isnacs 35592 mrefg2 35595 aomclem8 35965 islssfg2 35975 lnr2i 36021 pwelg 36210 stoweidlem50 38012 stoweidlem57 38019 issal 38276 omessle 38427 uhgreq12g 39298 uhgruhgra 39303 uhgrauhgr 39304 uhgr0vb 39308 isupgr 39319 isumgr 39328 isuspgr 39383 isusgr 39384 isausgr 39395 usgr1vr 39475 usgrexmpl 39481 nbuhgr2vtx1edgblem 39565 uhgeq12gALTV 40051 uhguhgra 40053 uhgrauhg 40054 uhg0v 40058 isfusgra 40105 |
Copyright terms: Public domain | W3C validator |