![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqimss | Unicode version |
Description: Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Ref | Expression |
---|---|
eqimss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqss 3170 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 274 |
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: eqimss2 3210 uneqin 3386 sssnr 3751 sssnm 3752 ssprr 3754 sstpr 3755 snsspw 3762 pwpwssunieq 3972 elpwuni 3973 disjeq2 3981 disjeq1 3984 pwne 4157 pwssunim 4280 poeq2 4296 seeq1 4335 seeq2 4336 trsucss 4419 onsucelsucr 4503 xp11m 5062 funeq 5231 fnresdm 5320 fssxp 5378 ffdm 5381 fcoi1 5391 fof 5433 dff1o2 5461 fvmptss2 5586 fvmptssdm 5595 fprg 5694 dff1o6 5770 tposeq 6241 el2oss1o 6437 nntri1 6490 nntri2or2 6492 nnsseleq 6495 infnninf 7115 infnninfOLD 7116 nninfwlpoimlemg 7166 exmidontri2or 7235 frec2uzf1od 10379 hashinfuni 10728 setsresg 12470 setsslid 12482 strle1g 12533 cncnpi 13361 hmeores 13448 limcimolemlt 13766 recnprss 13789 0nninf 14376 nninfall 14381 |
Copyright terms: Public domain | W3C validator |