![]() |
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 3098 | . 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
4 | 1, 3 | syl 14 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1481 ⊆ wss 3076 |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-in 3082 df-ss 3089 |
This theorem is referenced by: mptrcl 5511 riotacl 5752 riotasbc 5753 elmpocl 5976 ofrval 6000 f1od2 6140 mpoxopn0yelv 6144 tpostpos 6169 smores 6197 supubti 6894 suplubti 6895 prarloclemcalc 7334 rereceu 7721 recriota 7722 rexrd 7839 eqord1 8269 nnred 8757 nncnd 8758 un0addcl 9034 un0mulcl 9035 nnnn0d 9054 nn0red 9055 nn0xnn0d 9073 suprzclex 9173 nn0zd 9195 zred 9197 rpred 9513 ige2m1fz 9921 zmodfzp1 10152 seq3caopr2 10286 expcl2lemap 10336 m1expcl 10347 summodclem2a 11182 zsumdc 11185 clim2prod 11340 ntrivcvgap 11349 prodmodclem2a 11377 zproddc 11380 lcmn0cl 11785 ennnfonelemg 11952 lmrcl 12399 lmss 12454 upxp 12480 isxms2 12660 iooretopg 12736 tgqioo 12755 limccoap 12855 dvcl 12860 dvidlemap 12868 dvcnp2cntop 12871 isomninnlem 13400 trilpolemeq1 13408 trilpolemlt1 13409 iswomninnlem 13417 ismkvnnlem 13419 |
Copyright terms: Public domain | W3C validator |