![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fssd | GIF version |
Description: Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
fssd.f | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
fssd.b | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Ref | Expression |
---|---|
fssd | ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fssd.f | . 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
2 | fssd.b | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | |
3 | fss 5396 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) | |
4 | 1, 2, 3 | syl2anc 411 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3144 ⟶wf 5231 |
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 df-f 5239 |
This theorem is referenced by: mapss 6718 ac6sfi 6927 fseq1p1m1 10126 resqrexlemcvg 11063 resqrexlemsqa 11068 climcvg1nlem 11392 fsumcl2lem 11441 ennnfonelemh 12458 gsumress 12873 cnrest2 14213 cnptoprest2 14217 cncfss 14547 limccnpcntop 14621 dvcoapbr 14648 dvef 14665 isomninnlem 15257 trilpolemisumle 15265 iswomninnlem 15276 ismkvnnlem 15279 |
Copyright terms: Public domain | W3C validator |