Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqsstrd | Unicode version |
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
Ref | Expression |
---|---|
eqsstrd.1 | |
eqsstrd.2 |
Ref | Expression |
---|---|
eqsstrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsstrd.2 | . 2 | |
2 | eqsstrd.1 | . . 3 | |
3 | 2 | sseq1d 3166 | . 2 |
4 | 1, 3 | mpbird 166 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 wss 3111 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: eqsstrrd 3174 eqsstrdi 3189 tfisi 4558 funresdfunsnss 5682 suppssof1 6061 phplem4dom 6819 fival 6926 fiuni 6934 cardonle 7134 exmidfodomrlemim 7148 frecuzrdgtclt 10346 ennnfonelemkh 12282 ennnfonelemf1 12288 strfvssn 12353 setscom 12371 tgrest 12710 resttopon 12712 rest0 12720 lmtopcnp 12791 metequiv2 13037 xmettx 13051 ellimc3apf 13170 dvfvalap 13191 dvcjbr 13213 dvcj 13214 dvfre 13215 nnsf 13719 |
Copyright terms: Public domain | W3C validator |