![]() |
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 3096 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 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: sselii 3099 sseldi 3100 elun1 3248 elun2 3249 finds 4522 finds2 4523 issref 4929 2elresin 5242 fvun1 5495 fvmptssdm 5513 elfvmptrab1 5523 fvimacnvi 5542 elpreima 5547 ofrfval 5998 ofvalg 5999 off 6002 offres 6041 eqopi 6078 op1steq 6085 dfoprab4 6098 f1od2 6140 reldmtpos 6158 smores3 6198 smores2 6199 ctssdccl 7004 pinn 7141 indpi 7174 enq0enq 7263 preqlu 7304 elinp 7306 prop 7307 elnp1st2nd 7308 prarloclem5 7332 cauappcvgprlemladd 7490 peano5nnnn 7724 nnindnn 7725 recn 7777 rexr 7835 peano5nni 8747 nnre 8751 nncn 8752 nnind 8760 nnnn0 9008 nn0re 9010 nn0cn 9011 nn0xnn0 9068 nnz 9097 nn0z 9098 nnq 9452 qcn 9453 rpre 9477 iccshftri 9808 iccshftli 9810 iccdili 9812 icccntri 9814 fzval2 9824 fzelp1 9885 4fvwrd4 9948 elfzo1 9998 expcllem 10335 expcl2lemap 10336 m1expcl2 10346 bcm1k 10538 bcpasc 10544 cau3lem 10918 climconst2 11092 fsum3 11188 binomlem 11284 cos12dec 11510 dvdsflip 11585 infssuzcldc 11680 isprm3 11835 phimullem 11937 structcnvcnv 12014 fvsetsid 12032 tgval2 12259 qtopbasss 12729 dedekindicc 12819 ivthinc 12829 ivthdec 12830 cosz12 12909 cos0pilt1 12981 ioocosf1o 12983 exmidsbthrlem 13392 |
Copyright terms: Public domain | W3C validator |