Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fss | Unicode version |
Description: Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
fss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3144 | . . . . 5 | |
2 | 1 | com12 30 | . . . 4 |
3 | 2 | anim2d 335 | . . 3 |
4 | df-f 5186 | . . 3 | |
5 | df-f 5186 | . . 3 | |
6 | 3, 4, 5 | 3imtr4g 204 | . 2 |
7 | 6 | impcom 124 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wss 3111 crn 4599 wfn 5177 wf 5178 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 df-f 5186 |
This theorem is referenced by: fssd 5344 fconst6g 5380 f1ss 5393 ffoss 5458 fsn2 5653 ofco 6062 tposf2 6227 issmo2 6248 smoiso 6261 mapsn 6647 ssdomg 6735 omp1eomlem 7050 1fv 10064 fxnn0nninf 10363 abscn2 11242 recn2 11244 imcn2 11245 climabs 11247 climre 11249 climim 11250 fsumre 11399 fsumim 11400 ismet2 12901 dvfre 13221 dvrecap 13224 |
Copyright terms: Public domain | W3C validator |