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 5369 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) | |
4 | 1, 2, 3 | syl2anc 411 | 1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3127 ⟶wf 5204 |
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 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-11 1504 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-ext 2157 |
This theorem depends on definitions: df-bi 117 df-nf 1459 df-sb 1761 df-clab 2162 df-cleq 2168 df-clel 2171 df-in 3133 df-ss 3140 df-f 5212 |
This theorem is referenced by: mapss 6681 ac6sfi 6888 fseq1p1m1 10062 resqrexlemcvg 10995 resqrexlemsqa 11000 climcvg1nlem 11324 fsumcl2lem 11373 ennnfonelemh 12371 cnrest2 13229 cnptoprest2 13233 cncfss 13563 limccnpcntop 13637 dvcoapbr 13664 dvef 13681 isomninnlem 14261 trilpolemisumle 14269 iswomninnlem 14280 ismkvnnlem 14283 |
Copyright terms: Public domain | W3C validator |