![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseldi | GIF version |
Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
Ref | Expression |
---|---|
sseli.1 | ⊢ 𝐴 ⊆ 𝐵 |
sseldi.2 | ⊢ (𝜑 → 𝐶 ∈ 𝐴) |
Ref | Expression |
---|---|
sseldi | ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseldi.2 | . 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴) | |
2 | sseli.1 | . . 3 ⊢ 𝐴 ⊆ 𝐵 | |
3 | 2 | sseli 2996 | . 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
4 | 1, 3 | syl 14 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 ⊆ wss 2974 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-11 1438 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-in 2980 df-ss 2987 |
This theorem is referenced by: riotacl 5513 riotasbc 5514 elmpt2cl 5729 ofrval 5753 f1od2 5887 mpt2xopn0yelv 5888 tpostpos 5913 smores 5941 supubti 6471 suplubti 6472 prarloclemcalc 6754 rereceu 7117 recriota 7118 rexrd 7230 nnred 8119 nncnd 8120 un0addcl 8388 un0mulcl 8389 nnnn0d 8408 nn0red 8409 nn0xnn0d 8427 suprzclex 8526 nn0zd 8548 zred 8550 rpred 8854 ige2m1fz 9203 zmodfzp1 9430 iseqcaopr2 9557 expcl2lemap 9585 m1expcl 9596 lcmn0cl 10594 |
Copyright terms: Public domain | W3C validator |