Metamath Proof Explorer


Theorem frege102

Description: If Z belongs to the R -sequence beginning with X , then every result of an application of the procedure R to Z follows X in the R -sequence. Proposition 102 of Frege1879 p. 72. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege102.x X A
frege102.z Z B
frege102.v V C
frege102.r R D
Assertion frege102 X t+ R I Z Z R V X t+ R V

Proof

Step Hyp Ref Expression
1 frege102.x X A
2 frege102.z Z B
3 frege102.v V C
4 frege102.r R D
5 2 3 4 frege92 Z = X Z R V X t+ R V
6 1 2 3 4 frege96 X t+ R Z Z R V X t+ R V
7 2 frege101 Z = X Z R V X t+ R V X t+ R Z Z R V X t+ R V X t+ R I Z Z R V X t+ R V
8 5 6 7 mp2 X t+ R I Z Z R V X t+ R V