Theorem frege90

Description: Add antecedent to frege89 . Proposition 90 of Frege1879 p. 68. (Contributed by RP, 1-Jul-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		frege90.x	$$⊢X\in U$$
2		frege90.y	$$⊢Y\in V$$
3		frege90.r	$$⊢R\in W$$
4	1 2 3	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$$
5		frege5	$$⊢\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)\to \left(\left(\phi \to \forall f\left(Rhereditaryf\to \left(\forall w\left(XRw\to w\in f\right)\to Y\in f\right)\right)\right)\to \left(\phi \to X\mathrm{t+}\left(R\right)Y\right)\right)$$
6	4 5	ax-mp	$$⊢\left(\phi \to \forall f\left(Rhereditaryf\to \left(\forall w\left(XRw\to w\in f\right)\to Y\in f\right)\right)\right)\to \left(\phi \to X\mathrm{t+}\left(R\right)Y\right)$$