![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elpwid | Unicode version |
Description: An element of a power class is a subclass. Deduction form of elpwi 3596. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
elpwid.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elpwid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwid.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elpwi 3596 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-v 2751 df-in 3147 df-ss 3154 df-pw 3589 |
This theorem is referenced by: fopwdom 6850 ssenen 6865 fival 6983 fiuni 6991 3nelsucpw1 7247 elnp1st2nd 7489 ixxssxr 9914 elfzoelz 10161 restid2 12715 epttop 13886 neiss2 13938 blssm 14217 blin2 14228 cncfrss 14358 cncfrss2 14359 pwle2 15045 |
Copyright terms: Public domain | W3C validator |