Theorem frege120

Description: Simplified application of one direction of dffrege115 . Proposition 120 of Frege1879 p. 78. (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	frege120	|- ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege116.x	|- X e. U
2		frege118.y	|- Y e. V
3		frege120.a	|- A e. W
4	3	frege58c	|- ( A. a ( Y R a -> a = X ) -> [. A / a ]. ( Y R a -> a = X ) )
5		sbcim1	|- ( [. A / a ]. ( Y R a -> a = X ) -> ( [. A / a ]. Y R a -> [. A / a ]. a = X ) )
6		sbcbr2g	|- ( A e. W -> ( [. A / a ]. Y R a <-> Y R [_ A / a ]_ a ) )
7	3 6	ax-mp	|- ( [. A / a ]. Y R a <-> Y R [_ A / a ]_ a )
8		csbvarg	|- ( A e. W -> [_ A / a ]_ a = A )
9	3 8	ax-mp	|- [_ A / a ]_ a = A
10	9	breq2i	|- ( Y R [_ A / a ]_ a <-> Y R A )
11	7 10	bitri	|- ( [. A / a ]. Y R a <-> Y R A )
12		sbceq1g	|- ( A e. W -> ( [. A / a ]. a = X <-> [_ A / a ]_ a = X ) )
13	3 12	ax-mp	|- ( [. A / a ]. a = X <-> [_ A / a ]_ a = X )
14	9	eqeq1i	|- ( [_ A / a ]_ a = X <-> A = X )
15	13 14	bitri	|- ( [. A / a ]. a = X <-> A = X )
16	5 11 15	3imtr3g	|- ( [. A / a ]. ( Y R a -> a = X ) -> ( Y R A -> A = X ) )
17	4 16	syl	|- ( A. a ( Y R a -> a = X ) -> ( Y R A -> A = X ) )
18	1 2	frege119	|- ( ( A. a ( Y R a -> a = X ) -> ( Y R A -> A = X ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) ) )
19	17 18	ax-mp	|- ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) )