![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pwidg | Structured version Visualization version Unicode version |
Description: Membership of the original in a power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Ref | Expression |
---|---|
pwidg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3453 |
. 2
![]() ![]() ![]() ![]() | |
2 | elpwg 3961 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbiri 237 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-v 3049 df-in 3413 df-ss 3420 df-pw 3955 |
This theorem is referenced by: pwid 3967 axpweq 4583 knatar 6253 brwdom2 8093 pwwf 8283 rankpwi 8299 canthp1lem2 9083 canthp1 9084 grothpw 9256 mremre 15522 submre 15523 baspartn 19981 fctop 20031 cctop 20033 ppttop 20034 epttop 20036 isopn3 20094 mretopd 20120 tsmsfbas 21154 gsumesum 28892 esumcst 28896 pwsiga 28964 prsiga 28965 sigainb 28970 pwldsys 28991 ldgenpisyslem1 28997 carsggect 29162 neibastop1 31027 neibastop2lem 31028 topdifinfindis 31761 elrfi 35548 pwssfi 37391 dvnprodlem3 37833 caragenunidm 38339 |
Copyright terms: Public domain | W3C validator |