Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sselid | GIF version |
Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
Ref | Expression |
---|---|
sseli.1 | ⊢ 𝐴 ⊆ 𝐵 |
sselid.2 | ⊢ (𝜑 → 𝐶 ∈ 𝐴) |
Ref | Expression |
---|---|
sselid | ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sselid.2 | . 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴) | |
2 | sseli.1 | . . 3 ⊢ 𝐴 ⊆ 𝐵 | |
3 | 2 | sseli 3143 | . 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
4 | 1, 3 | syl 14 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ⊆ wss 3121 |
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 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134 |
This theorem is referenced by: mptrcl 5576 riotacl 5820 riotasbc 5821 elmpocl 6044 ofrval 6068 f1od2 6211 mpoxopn0yelv 6215 tpostpos 6240 smores 6268 supubti 6972 suplubti 6973 prarloclemcalc 7451 rereceu 7838 recriota 7839 rexrd 7956 eqord1 8389 nnred 8878 nncnd 8879 un0addcl 9155 un0mulcl 9156 nnnn0d 9175 nn0red 9176 nn0xnn0d 9194 suprzclex 9297 nn0zd 9319 zred 9321 rpred 9640 ige2m1fz 10053 zmodfzp1 10291 seq3caopr2 10425 expcl2lemap 10475 m1expcl 10486 summodclem2a 11331 zsumdc 11334 clim2prod 11489 ntrivcvgap 11498 prodmodclem2a 11526 zproddc 11529 zsupssdc 11896 lcmn0cl 12009 isprm5lem 12082 eulerthlemrprm 12170 eulerthlema 12171 eulerthlemh 12172 eulerthlemth 12173 prmdivdiv 12178 ennnfonelemg 12345 lmrcl 12944 lmss 12999 upxp 13025 isxms2 13205 iooretopg 13281 tgqioo 13300 limccoap 13400 dvcl 13405 dvidlemap 13413 dvcnp2cntop 13416 lgscl 13668 2sqlem6 13709 2sqlem8 13712 2sqlem9 13713 isomninnlem 14022 trilpolemeq1 14032 trilpolemlt1 14033 iswomninnlem 14041 iswomni0 14043 ismkvnnlem 14044 nconstwlpolemgt0 14055 |
Copyright terms: Public domain | W3C validator |