![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseqtrd | Unicode version |
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
Ref | Expression |
---|---|
sseqtrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
sseqtrd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sseqtrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqtrd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sseqtrd.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | sseq2d 3197 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbid 147 |
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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-11 1516 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-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-in 3147 df-ss 3154 |
This theorem is referenced by: sseqtrrd 3206 fssdmd 5391 resasplitss 5407 nnaword2 6529 erssxp 6572 phpm 6879 nnnninfeq 7140 ioodisj 10007 subsubm 12896 subsubg 13097 trivsubgd 13100 trivnsgd 13117 subsubrng 13491 subrgugrp 13517 subsubrg 13522 islssmd 13605 lspun 13648 lspssp 13649 lsslsp 13675 tgcl 13917 basgen 13933 bastop1 13936 bastop2 13937 clsss2 13982 topssnei 14015 cnntr 14078 txbasval 14120 neitx 14121 cnmpt1res 14149 cnmpt2res 14150 imasnopn 14152 hmeontr 14166 tgioo 14399 reldvg 14501 dvfvalap 14503 dvbss 14507 dvcnp2cntop 14516 dvaddxxbr 14518 dvmulxxbr 14519 dvcj 14526 |
Copyright terms: Public domain | W3C validator |