Metamath Proof Explorer


Theorem frege122d

Description: If F is a function, A is the successor of X , and B is the successor of X , then A and B are the same (or B follows A in the transitive closure of F ). Similar to Proposition 122 of Frege1879 p. 79. Compare with frege122 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypotheses frege122d.a φ A = F X
frege122d.b φ B = F X
Assertion frege122d φ A t+ F B A = B

Proof

Step Hyp Ref Expression
1 frege122d.a φ A = F X
2 frege122d.b φ B = F X
3 1 2 eqtr4d φ A = B
4 3 olcd φ A t+ F B A = B