Theorem frege91d

Description: If B follows A in R then B follows A in the transitive closure of R . Similar to Proposition 91 of Frege1879 p. 68. Comparw with frege91 . (Contributed by RP, 15-Jul-2020)

	Ref	Expression
Hypotheses	frege91d.r	$$⊢\phi \to R\in \mathrm{V}$$
	frege91d.ac	$$⊢\phi \to ARB$$
Assertion	frege91d	$$⊢\phi \to A\mathrm{t+}\left(R\right)B$$

Proof

Step	Hyp	Ref	Expression
1		frege91d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		frege91d.ac	$$⊢\phi \to ARB$$
3		trclfvlb	$$⊢R\in \mathrm{V}\to R\subseteq \mathrm{t+}\left(R\right)$$
4	1 3	syl	$$⊢\phi \to R\subseteq \mathrm{t+}\left(R\right)$$
5	4	ssbrd	$$⊢\phi \to \left(ARB\to A\mathrm{t+}\left(R\right)B\right)$$
6	2 5	mpd	$$⊢\phi \to A\mathrm{t+}\left(R\right)B$$