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 5578 riotacl 5823 riotasbc 5824 elmpocl 6047 ofrval 6071 f1od2 6214 mpoxopn0yelv 6218 tpostpos 6243 smores 6271 supubti 6976 suplubti 6977 nninfwlporlemd 7148 nninfwlporlem 7149 nninfwlpoimlemg 7151 nninfwlpoimlemginf 7152 prarloclemcalc 7464 rereceu 7851 recriota 7852 rexrd 7969 eqord1 8402 nnred 8891 nncnd 8892 un0addcl 9168 un0mulcl 9169 nnnn0d 9188 nn0red 9189 nn0xnn0d 9207 suprzclex 9310 nn0zd 9332 zred 9334 rpred 9653 ige2m1fz 10066 zmodfzp1 10304 seq3caopr2 10438 expcl2lemap 10488 m1expcl 10499 summodclem2a 11344 zsumdc 11347 clim2prod 11502 ntrivcvgap 11511 prodmodclem2a 11539 zproddc 11542 zsupssdc 11909 lcmn0cl 12022 isprm5lem 12095 eulerthlemrprm 12183 eulerthlema 12184 eulerthlemh 12185 eulerthlemth 12186 prmdivdiv 12191 ennnfonelemg 12358 lmrcl 12985 lmss 13040 upxp 13066 isxms2 13246 iooretopg 13322 tgqioo 13341 limccoap 13441 dvcl 13446 dvidlemap 13454 dvcnp2cntop 13457 lgscl 13709 2sqlem6 13750 2sqlem8 13753 2sqlem9 13754 isomninnlem 14062 trilpolemeq1 14072 trilpolemlt1 14073 iswomninnlem 14081 iswomni0 14083 ismkvnnlem 14084 nconstwlpolemgt0 14095 |
Copyright terms: Public domain | W3C validator |