Metamath Proof Explorer


Theorem frege124

Description: If X is a result of an application of the single-valued procedure R to Y and if M follows Y in the R -sequence, then M belongs to the R -sequence beginning with X . Proposition 124 of Frege1879 p. 80. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege123.x X U
frege123.y Y V
frege124.m M W
frege124.r R S
Assertion frege124 Fun R -1 -1 Y R X Y t+ R M X t+ R I M

Proof

Step Hyp Ref Expression
1 frege123.x X U
2 frege123.y Y V
3 frege124.m M W
4 frege124.r R S
5 1 2 3 4 frege110 a Y R a X t+ R I a Y t+ R M X t+ R I M
6 1 2 frege123 a Y R a X t+ R I a Y t+ R M X t+ R I M Fun R -1 -1 Y R X Y t+ R M X t+ R I M
7 5 6 ax-mp Fun R -1 -1 Y R X Y t+ R M X t+ R I M