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

Proof

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