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 e. U
	frege90.y	|- Y e. V
	frege90.r	|- R e. W
Assertion	frege90	|- ( ( ph -> A. f ( R hereditary f -> ( A. w ( X R w -> w e. f ) -> Y e. f ) ) ) -> ( ph -> X ( t+ ` R ) Y ) )

Proof

Step	Hyp	Ref	Expression
1		frege90.x	|- X e. U
2		frege90.y	|- Y e. V
3		frege90.r	|- R e. W
4	1 2 3	frege89	|- ( A. f ( R hereditary f -> ( A. w ( X R w -> w e. f ) -> Y e. f ) ) -> X ( t+ ` R ) Y )
5		frege5	|- ( ( A. f ( R hereditary f -> ( A. w ( X R w -> w e. f ) -> Y e. f ) ) -> X ( t+ ` R ) Y ) -> ( ( ph -> A. f ( R hereditary f -> ( A. w ( X R w -> w e. f ) -> Y e. f ) ) ) -> ( ph -> X ( t+ ` R ) Y ) ) )
6	4 5	ax-mp	|- ( ( ph -> A. f ( R hereditary f -> ( A. w ( X R w -> w e. f ) -> Y e. f ) ) ) -> ( ph -> X ( t+ ` R ) Y ) )