Description: If X is a result of an application of the single-valued procedure R to Y , then every result of an application of the procedure R to Y belongs to the R -sequence beginning with X . Proposition 122 of Frege1879 p. 79. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | frege116.x | |- X e. U |
|
| frege118.y | |- Y e. V |
||
| frege120.a | |- A e. W |
||
| Assertion | frege122 | |- ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frege116.x | |- X e. U |
|
| 2 | frege118.y | |- Y e. V |
|
| 3 | frege120.a | |- A e. W |
|
| 4 | 3 | frege112 | |- ( A = X -> X ( ( t+ ` R ) u. _I ) A ) |
| 5 | 1 2 3 | frege121 | |- ( ( A = X -> X ( ( t+ ` R ) u. _I ) A ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) ) ) |
| 6 | 4 5 | ax-mp | |- ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) ) |