![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseqtri | GIF version |
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.) |
Ref | Expression |
---|---|
sseqtr.1 | ⊢ 𝐴 ⊆ 𝐵 |
sseqtr.2 | ⊢ 𝐵 = 𝐶 |
Ref | Expression |
---|---|
sseqtri | ⊢ 𝐴 ⊆ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqtr.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | sseqtr.2 | . . 3 ⊢ 𝐵 = 𝐶 | |
3 | 2 | sseq2i 3182 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶) |
4 | 1, 3 | mpbi 145 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1353 ⊆ wss 3129 |
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: sseqtrri 3190 eqimssi 3211 abssi 3230 ssun2 3299 inssddif 3376 difdifdirss 3507 ifidss 3549 pwundifss 4281 unixpss 4735 0ima 4983 sbthlem7 6955 ssnnctlemct 12417 toponsspwpwg 13153 eltg4i 13188 ntrss2 13254 isopn3 13258 tgioo 13679 dvfvalap 13783 dvcnp2cntop 13796 |
Copyright terms: Public domain | W3C validator |