Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sseq1i | Unicode version |
Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.) |
Ref | Expression |
---|---|
sseq1i.1 |
Ref | Expression |
---|---|
sseq1i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1i.1 | . 2 | |
2 | sseq1 3170 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wceq 1348 wss 3121 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134 |
This theorem is referenced by: eqsstri 3179 eqsstrid 3193 ssab 3217 rabss 3224 uniiunlem 3236 prss 3734 prssg 3735 tpss 3743 iunss 3912 pwtr 4202 ordsucss 4486 elomssom 4587 cores2 5121 dffun2 5206 funimaexglem 5279 idref 5733 ordgt0ge1 6411 3nsssucpw1 7200 prarloclemn 7448 bdeqsuc 13876 bj-omssind 13930 |
Copyright terms: Public domain | W3C validator |