![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseli | GIF version |
Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sseli.1 | ⊢ 𝐴 ⊆ 𝐵 |
Ref | Expression |
---|---|
sseli | ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseli.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | ssel 3164 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ⊆ wss 3144 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 |
This theorem is referenced by: sselii 3167 sselid 3168 elun1 3317 elun2 3318 finds 4614 finds2 4615 issref 5026 2elresin 5343 fvun1 5599 fvmptssdm 5617 elfvmptrab1 5627 fvimacnvi 5647 elpreima 5652 ofrfval 6110 ofvalg 6111 off 6114 offres 6155 eqopi 6192 op1steq 6199 dfoprab4 6212 f1od2 6255 reldmtpos 6273 smores3 6313 smores2 6314 ctssdccl 7135 pinn 7333 indpi 7366 enq0enq 7455 preqlu 7496 elinp 7498 prop 7499 elnp1st2nd 7500 prarloclem5 7524 cauappcvgprlemladd 7682 peano5nnnn 7916 nnindnn 7917 recn 7969 rexr 8028 peano5nni 8947 nnre 8951 nncn 8952 nnind 8960 nnnn0 9208 nn0re 9210 nn0cn 9211 nn0xnn0 9268 nnz 9297 nn0z 9298 nnq 9658 qcn 9659 rpre 9685 iccshftri 10020 iccshftli 10022 iccdili 10024 icccntri 10026 fzval2 10036 fzelp1 10099 4fvwrd4 10165 elfzo1 10215 expcllem 10557 expcl2lemap 10558 m1expcl2 10568 bcm1k 10767 bcpasc 10773 cau3lem 11150 climconst2 11326 fsum3 11422 binomlem 11518 fprodge1 11674 cos12dec 11802 dvdsflip 11884 infssuzcldc 11979 isprm3 12145 phimullem 12252 prmdiveq 12263 structcnvcnv 12523 fvsetsid 12541 ptex 12762 nmzsubg 13142 nmznsg 13145 nzrring 13526 lringnzr 13533 rege0subm 13880 tgval2 13988 qtopbasss 14458 dedekindicc 14548 ivthinc 14558 ivthdec 14559 cosz12 14638 cos0pilt1 14710 ioocosf1o 14712 exmidsbthrlem 15209 |
Copyright terms: Public domain | W3C validator |