![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sseq1i | Structured version Visualization version 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 3465 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-in 3423 df-ss 3430 |
This theorem is referenced by: eqsstri 3474 syl5eqss 3488 ssab 3511 rabss 3518 uniiunlem 3529 prss 4139 prssg 4140 sstp 4149 tpss 4150 iunss 4333 pwtr 4670 pwssun 4762 cores2 5371 sspred 5411 dffun2 5615 sbcfg 5753 idref 6176 ovmptss 6909 fnsuppres 6974 ordgt0ge1 7230 omopthlem1 7387 trcl 8243 rankbnd 8370 rankbnd2 8371 rankc1 8372 dfac12a 8609 fin23lem34 8807 axdc2lem 8909 alephval2 9028 indpi 9363 fsuppmapnn0fiublem 12240 0ram 15033 mreacs 15619 lsslinds 19444 2ndcctbss 20525 xkoinjcn 20757 restmetu 21640 xrlimcnp 23950 mptelee 24981 ausisusgra 25138 frgraunss 25779 n4cyclfrgra 25802 shlesb1i 27095 mdsldmd1i 28040 csmdsymi 28043 dfon2lem3 30481 dfon2lem7 30485 trpredmintr 30522 filnetlem4 31087 ptrecube 31986 poimirlem30 32016 undmrnresiss 36256 clcnvlem 36276 ss2iundf 36297 cnvtrrel 36308 brtrclfv2 36365 rp-imass 36412 dfhe3 36416 dffrege76 36581 iunssf 37481 iunopeqop 39141 ausgrusgrb 39396 nbuhgr2vtx1edgblem 39565 nbgrsym 39583 isuvtxa 39613 21wlkdlem6 39976 |
Copyright terms: Public domain | W3C validator |