![]() |
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 3020 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1439 ⊆ wss 3000 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-11 1443 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-in 3006 df-ss 3013 |
This theorem is referenced by: sselii 3023 sseldi 3024 elun1 3168 elun2 3169 finds 4428 finds2 4429 issref 4827 2elresin 5138 fvun1 5383 fvmptssdm 5400 fvimacnvi 5427 elpreima 5432 ofrfval 5878 fnofval 5879 off 5882 offres 5920 eqopi 5956 op1steq 5963 dfoprab4 5976 f1od2 6014 reldmtpos 6032 smores3 6072 smores2 6073 pinn 6929 indpi 6962 enq0enq 7051 preqlu 7092 elinp 7094 prop 7095 elnp1st2nd 7096 prarloclem5 7120 cauappcvgprlemladd 7278 peano5nnnn 7488 nnindnn 7489 recn 7536 rexr 7594 peano5nni 8486 nnre 8490 nncn 8491 nnind 8499 nnnn0 8741 nn0re 8743 nn0cn 8744 nn0xnn0 8801 nnz 8830 nn0z 8831 nnq 9179 qcn 9180 rpre 9201 iccshftri 9473 iccshftli 9475 iccdili 9477 icccntri 9479 fzval2 9488 fzelp1 9549 4fvwrd4 9612 elfzo1 9662 expcllem 10027 expcl2lemap 10028 m1expcl2 10038 bcm1k 10229 bcpasc 10235 cau3lem 10608 climconst2 10740 fisum 10839 binomlem 10938 dvdsflip 11191 infssuzcldc 11286 isprm3 11439 phimullem 11540 structcnvcnv 11571 fvsetsid 11589 tgval2 11812 exmidsbthrlem 12184 |
Copyright terms: Public domain | W3C validator |