![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqimss2 | Unicode version |
Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.) |
Ref | Expression |
---|---|
eqimss2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss 3209 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eqcoms 2180 |
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-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: disjeq2 3984 disjeq1 3987 poeq2 4300 seeq1 4339 seeq2 4340 dmcoeq 4899 xp11m 5067 funeq 5236 fconst3m 5735 tposeq 6247 undifdcss 6921 ennnfonelemk 12395 ennnfonelemss 12405 qnnen 12426 imasaddfnlemg 12717 topgele 13420 topontopn 13428 txdis 13670 |
Copyright terms: Public domain | W3C validator |