Metamath Proof Explorer

Theorem frege116

Description: One direction of dffrege115 . Proposition 116 of Frege1879 p. 77. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege116.x 
|- X e. U
Assertion frege116 
|- ( Fun `' `' R -> A. b ( b R X -> A. a ( b R a -> a = X ) ) )

Proof

Step Hyp Ref Expression
1 frege116.x 
 |-  X e. U
2 dffrege115 
 |-  ( A. c A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> Fun `' `' R )
3 1 frege68c 
 |-  ( ( A. c A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> Fun `' `' R ) -> ( Fun `' `' R -> [. X / c ]. A. b ( b R c -> A. a ( b R a -> a = c ) ) ) )
4 sbcal 
 |-  ( [. X / c ]. A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> A. b [. X / c ]. ( b R c -> A. a ( b R a -> a = c ) ) )
5 sbcimg 
 |-  ( X e. U -> ( [. X / c ]. ( b R c -> A. a ( b R a -> a = c ) ) <-> ( [. X / c ]. b R c -> [. X / c ]. A. a ( b R a -> a = c ) ) ) )
6 1 5 ax-mp 
 |-  ( [. X / c ]. ( b R c -> A. a ( b R a -> a = c ) ) <-> ( [. X / c ]. b R c -> [. X / c ]. A. a ( b R a -> a = c ) ) )
7 sbcbr2g 
 |-  ( X e. U -> ( [. X / c ]. b R c <-> b R [_ X / c ]_ c ) )
8 1 7 ax-mp 
 |-  ( [. X / c ]. b R c <-> b R [_ X / c ]_ c )
9 csbvarg 
 |-  ( X e. U -> [_ X / c ]_ c = X )
10 1 9 ax-mp 
 |-  [_ X / c ]_ c = X
11 10 breq2i 
 |-  ( b R [_ X / c ]_ c <-> b R X )
12 8 11 bitri 
 |-  ( [. X / c ]. b R c <-> b R X )
13 sbcal 
 |-  ( [. X / c ]. A. a ( b R a -> a = c ) <-> A. a [. X / c ]. ( b R a -> a = c ) )
14 sbcimg 
 |-  ( X e. U -> ( [. X / c ]. ( b R a -> a = c ) <-> ( [. X / c ]. b R a -> [. X / c ]. a = c ) ) )
15 1 14 ax-mp 
 |-  ( [. X / c ]. ( b R a -> a = c ) <-> ( [. X / c ]. b R a -> [. X / c ]. a = c ) )
16 sbcg 
 |-  ( X e. U -> ( [. X / c ]. b R a <-> b R a ) )
17 1 16 ax-mp 
 |-  ( [. X / c ]. b R a <-> b R a )
18 sbceq2g 
 |-  ( X e. U -> ( [. X / c ]. a = c <-> a = [_ X / c ]_ c ) )
19 1 18 ax-mp 
 |-  ( [. X / c ]. a = c <-> a = [_ X / c ]_ c )
20 10 eqeq2i 
 |-  ( a = [_ X / c ]_ c <-> a = X )
21 19 20 bitri 
 |-  ( [. X / c ]. a = c <-> a = X )
22 17 21 imbi12i 
 |-  ( ( [. X / c ]. b R a -> [. X / c ]. a = c ) <-> ( b R a -> a = X ) )
23 15 22 bitri 
 |-  ( [. X / c ]. ( b R a -> a = c ) <-> ( b R a -> a = X ) )
24 23 albii 
 |-  ( A. a [. X / c ]. ( b R a -> a = c ) <-> A. a ( b R a -> a = X ) )
25 13 24 bitri 
 |-  ( [. X / c ]. A. a ( b R a -> a = c ) <-> A. a ( b R a -> a = X ) )
26 12 25 imbi12i 
 |-  ( ( [. X / c ]. b R c -> [. X / c ]. A. a ( b R a -> a = c ) ) <-> ( b R X -> A. a ( b R a -> a = X ) ) )
27 6 26 bitri 
 |-  ( [. X / c ]. ( b R c -> A. a ( b R a -> a = c ) ) <-> ( b R X -> A. a ( b R a -> a = X ) ) )
28 27 albii 
 |-  ( A. b [. X / c ]. ( b R c -> A. a ( b R a -> a = c ) ) <-> A. b ( b R X -> A. a ( b R a -> a = X ) ) )
29 4 28 bitri 
 |-  ( [. X / c ]. A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> A. b ( b R X -> A. a ( b R a -> a = X ) ) )
30 3 29 syl6ib 
 |-  ( ( A. c A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> Fun `' `' R ) -> ( Fun `' `' R -> A. b ( b R X -> A. a ( b R a -> a = X ) ) ) )
31 2 30 ax-mp 
 |-  ( Fun `' `' R -> A. b ( b R X -> A. a ( b R a -> a = X ) ) )