Metamath Proof Explorer

Theorem frege117

Description: Lemma for frege118 . Proposition 117 of Frege1879 p. 78. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege116.x 
|- X e. U
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 frege116.x 
 |-  X e. U
2 1 frege116 
 |-  ( Fun `' `' R -> A. b ( b R X -> A. a ( b R a -> a = X ) ) )
3 frege9 
 |-  ( ( Fun `' `' R -> A. b ( b R X -> A. a ( b R a -> a = X ) ) ) -> ( ( 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 ) ) ) ) )
4 2 3 ax-mp 
 |-  ( ( 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 ) ) ) )