Theorem frege118

Description: Simplified application of one direction of dffrege115 . Proposition 118 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
Assertion	frege118	|- ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> a = X ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege116.x	|- X e. U
2		frege118.y	|- Y e. V
3	2	frege58c	|- ( A. b ( b R X -> A. a ( b R a -> a = X ) ) -> [. Y / b ]. ( b R X -> A. a ( b R a -> a = X ) ) )
4		sbcimg	|- ( Y e. V -> ( [. Y / b ]. ( b R X -> A. a ( b R a -> a = X ) ) <-> ( [. Y / b ]. b R X -> [. Y / b ]. A. a ( b R a -> a = X ) ) ) )
5	2 4	ax-mp	|- ( [. Y / b ]. ( b R X -> A. a ( b R a -> a = X ) ) <-> ( [. Y / b ]. b R X -> [. Y / b ]. A. a ( b R a -> a = X ) ) )
6		sbcbr1g	|- ( Y e. V -> ( [. Y / b ]. b R X <-> [_ Y / b ]_ b R X ) )
7	2 6	ax-mp	|- ( [. Y / b ]. b R X <-> [_ Y / b ]_ b R X )
8		csbvarg	|- ( Y e. V -> [_ Y / b ]_ b = Y )
9	2 8	ax-mp	|- [_ Y / b ]_ b = Y
10	9	breq1i	|- ( [_ Y / b ]_ b R X <-> Y R X )
11	7 10	bitri	|- ( [. Y / b ]. b R X <-> Y R X )
12		sbcal	|- ( [. Y / b ]. A. a ( b R a -> a = X ) <-> A. a [. Y / b ]. ( b R a -> a = X ) )
13		sbcimg	|- ( Y e. V -> ( [. Y / b ]. ( b R a -> a = X ) <-> ( [. Y / b ]. b R a -> [. Y / b ]. a = X ) ) )
14	2 13	ax-mp	|- ( [. Y / b ]. ( b R a -> a = X ) <-> ( [. Y / b ]. b R a -> [. Y / b ]. a = X ) )
15		sbcbr1g	|- ( Y e. V -> ( [. Y / b ]. b R a <-> [_ Y / b ]_ b R a ) )
16	2 15	ax-mp	|- ( [. Y / b ]. b R a <-> [_ Y / b ]_ b R a )
17	9	breq1i	|- ( [_ Y / b ]_ b R a <-> Y R a )
18	16 17	bitri	|- ( [. Y / b ]. b R a <-> Y R a )
19		sbcg	|- ( Y e. V -> ( [. Y / b ]. a = X <-> a = X ) )
20	2 19	ax-mp	|- ( [. Y / b ]. a = X <-> a = X )
21	18 20	imbi12i	|- ( ( [. Y / b ]. b R a -> [. Y / b ]. a = X ) <-> ( Y R a -> a = X ) )
22	14 21	bitri	|- ( [. Y / b ]. ( b R a -> a = X ) <-> ( Y R a -> a = X ) )
23	22	albii	|- ( A. a [. Y / b ]. ( b R a -> a = X ) <-> A. a ( Y R a -> a = X ) )
24	12 23	bitri	|- ( [. Y / b ]. A. a ( b R a -> a = X ) <-> A. a ( Y R a -> a = X ) )
25	11 24	imbi12i	|- ( ( [. Y / b ]. b R X -> [. Y / b ]. A. a ( b R a -> a = X ) ) <-> ( Y R X -> A. a ( Y R a -> a = X ) ) )
26	5 25	bitri	|- ( [. Y / b ]. ( b R X -> A. a ( b R a -> a = X ) ) <-> ( Y R X -> A. a ( Y R a -> a = X ) ) )
27	3 26	sylib	|- ( A. b ( b R X -> A. a ( b R a -> a = X ) ) -> ( Y R X -> A. a ( Y R a -> a = X ) ) )
28	1	frege117	|- ( ( A. b ( b R X -> A. a ( b R a -> a = X ) ) -> ( Y R X -> A. a ( Y R a -> a = X ) ) ) -> ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> a = X ) ) ) )
29	27 28	ax-mp	|- ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> a = X ) ) )