Theorem frege121

Description: Lemma for frege122 . Proposition 121 of Frege1879 p. 79. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege116.x	|- X e. U
	frege118.y	|- Y e. V
	frege120.a	|- A e. W
Assertion	frege121	|- ( ( A = X -> X ( ( t+ ` R ) u. _I ) A ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege116.x	|- X e. U
2		frege118.y	|- Y e. V
3		frege120.a	|- A e. W
4	1 2 3	frege120	|- ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) )
5		frege20	|- ( ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) ) -> ( ( A = X -> X ( ( t+ ` R ) u. _I ) A ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) ) ) )
6	4 5	ax-mp	|- ( ( A = X -> X ( ( t+ ` R ) u. _I ) A ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) ) )