![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseldd | GIF version |
Description: Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.) |
Ref | Expression |
---|---|
sseld.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
sseldd.2 | ⊢ (𝜑 → 𝐶 ∈ 𝐴) |
Ref | Expression |
---|---|
sseldd | ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseldd.2 | . 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴) | |
2 | sseld.1 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
3 | 2 | sseld 3046 | . 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
4 | 1, 3 | mpd 13 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1448 ⊆ wss 3021 |
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 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-11 1452 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-in 3027 df-ss 3034 |
This theorem is referenced by: disjiun 3870 exmid01 4061 frirrg 4210 ordtri2or2exmid 4424 riotass 5689 tfrcldm 6190 nntr2 6329 eroveu 6450 eroprf 6452 ixpssmapg 6552 findcard2d 6714 findcard2sd 6715 fimax2gtrilemstep 6723 undifdc 6741 fisseneq 6749 fidcenumlemrks 6769 fidcenumlemr 6771 suplub2ti 6803 ctssdclemn0 6910 nnppipi 7052 archnqq 7126 prarloclemlt 7202 suprubex 8567 suprzclex 9001 fzssp1 9688 elfzoelz 9765 fzofzp1 9845 fzostep1 9855 frecuzrdgg 10030 frecuzrdgdomlem 10031 frecuzrdgsuctlem 10037 ser3mono 10092 bcm1k 10347 fimaxq 10414 leisorel 10421 zfz1isolemiso 10423 seq3coll 10426 fimaxre2 10837 summodclem2a 10989 fsum3cvg3 11004 fsumcl2lem 11006 fsum0diaglem 11048 fsumiun 11085 zssinfcl 11436 ennnfonelemhom 11720 exmidunben 11731 strsetsid 11774 strslssd 11787 topssnei 12113 cnprcl2k 12156 cnss1 12176 cnptopresti 12188 cnptoprest 12189 lmres 12198 txopn 12215 txcnp 12221 xmetres2 12307 blin2 12360 blopn 12418 elcncf2 12474 cncfmet 12492 cncfmptc 12495 cncfmptid 12496 negcncf 12500 mulcncflem 12502 limcimolemlt 12513 cnplimcim 12516 cnlimci 12518 limccnpcntop 12520 dvlemap 12522 dvfgg 12530 |
Copyright terms: Public domain | W3C validator |