Theorem frege89

Description: One direction of dffrege76 . Proposition 89 of Frege1879 p. 68. (Contributed by RP, 1-Jul-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege89.x	$$⊢X\in U$$
	frege89.y	$$⊢Y\in V$$
	frege89.r	$$⊢R\in W$$
Assertion	frege89	$$⊢\forall f\left(Rhereditaryf\to \left(\forall w\left(XRw\to w\in f\right)\to Y\in f\right)\right)\to X\mathrm{t+}\left(R\right)Y$$

Proof

Step	Hyp	Ref	Expression
1		frege89.x	$$⊢X\in U$$
2		frege89.y	$$⊢Y\in V$$
3		frege89.r	$$⊢R\in W$$
4	1 2 3	dffrege76	$$⊢\forall f\left(Rhereditaryf\to \left(\forall w\left(XRw\to w\in f\right)\to Y\in f\right)\right)\leftrightarrow X\mathrm{t+}\left(R\right)Y$$
5		frege52aid	$$⊢\left(\forall f\left(Rhereditaryf\to \left(\forall w\left(XRw\to w\in f\right)\to Y\in f\right)\right)\leftrightarrow X\mathrm{t+}\left(R\right)Y\right)\to \left(\forall f\left(Rhereditaryf\to \left(\forall w\left(XRw\to w\in f\right)\to Y\in f\right)\right)\to X\mathrm{t+}\left(R\right)Y\right)$$
6	4 5	ax-mp	$$⊢\forall f\left(Rhereditaryf\to \left(\forall w\left(XRw\to w\in f\right)\to Y\in f\right)\right)\to X\mathrm{t+}\left(R\right)Y$$