Metamath Proof Explorer

Theorem frege92

Description: Inference from frege91 . Proposition 92 of Frege1879 p. 69. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege91.x 
|- X e. U
frege91.y 
|- Y e. V
frege91.r 
|- R e. W
Assertion frege92 
|- ( X = Z -> ( X R Y -> Z ( t+ ` R ) Y ) )

Proof

Step Hyp Ref Expression
1 frege91.x 
 |-  X e. U
2 frege91.y 
 |-  Y e. V
3 frege91.r 
 |-  R e. W
4 vex 
 |-  w e. _V
5 4 2 3 frege91 
 |-  ( w R Y -> w ( t+ ` R ) Y )
6 5 sbcth 
 |-  ( X e. U -> [. X / w ]. ( w R Y -> w ( t+ ` R ) Y ) )
7 frege53c 
 |-  ( [. X / w ]. ( w R Y -> w ( t+ ` R ) Y ) -> ( X = Z -> [. Z / w ]. ( w R Y -> w ( t+ ` R ) Y ) ) )
8 6 7 syl 
 |-  ( X e. U -> ( X = Z -> [. Z / w ]. ( w R Y -> w ( t+ ` R ) Y ) ) )
9 sbcim1 
 |-  ( [. Z / w ]. ( w R Y -> w ( t+ ` R ) Y ) -> ( [. Z / w ]. w R Y -> [. Z / w ]. w ( t+ ` R ) Y ) )
10 9 imim2i 
 |-  ( ( X = Z -> [. Z / w ]. ( w R Y -> w ( t+ ` R ) Y ) ) -> ( X = Z -> ( [. Z / w ]. w R Y -> [. Z / w ]. w ( t+ ` R ) Y ) ) )
11 dfsbcq 
 |-  ( X = Z -> ( [. X / w ]. w R Y <-> [. Z / w ]. w R Y ) )
12 sbcbr1g 
 |-  ( X e. U -> ( [. X / w ]. w R Y <-> [_ X / w ]_ w R Y ) )
13 csbvarg 
 |-  ( X e. U -> [_ X / w ]_ w = X )
14 13 breq1d 
 |-  ( X e. U -> ( [_ X / w ]_ w R Y <-> X R Y ) )
15 12 14 bitrd 
 |-  ( X e. U -> ( [. X / w ]. w R Y <-> X R Y ) )
16 1 15 ax-mp 
 |-  ( [. X / w ]. w R Y <-> X R Y )
17 11 16 bitr3di 
 |-  ( X = Z -> ( [. Z / w ]. w R Y <-> X R Y ) )
18 eqcom 
 |-  ( X = Z <-> Z = X )
19 18 biimpi 
 |-  ( X = Z -> Z = X )
20 19 1 eqeltrdi 
 |-  ( X = Z -> Z e. U )
21 sbcbr1g 
 |-  ( Z e. U -> ( [. Z / w ]. w ( t+ ` R ) Y <-> [_ Z / w ]_ w ( t+ ` R ) Y ) )
22 csbvarg 
 |-  ( Z e. U -> [_ Z / w ]_ w = Z )
23 22 breq1d 
 |-  ( Z e. U -> ( [_ Z / w ]_ w ( t+ ` R ) Y <-> Z ( t+ ` R ) Y ) )
24 21 23 bitrd 
 |-  ( Z e. U -> ( [. Z / w ]. w ( t+ ` R ) Y <-> Z ( t+ ` R ) Y ) )
25 20 24 syl 
 |-  ( X = Z -> ( [. Z / w ]. w ( t+ ` R ) Y <-> Z ( t+ ` R ) Y ) )
26 17 25 imbi12d 
 |-  ( X = Z -> ( ( [. Z / w ]. w R Y -> [. Z / w ]. w ( t+ ` R ) Y ) <-> ( X R Y -> Z ( t+ ` R ) Y ) ) )
27 10 26 mpbidi 
 |-  ( ( X = Z -> [. Z / w ]. ( w R Y -> w ( t+ ` R ) Y ) ) -> ( X = Z -> ( X R Y -> Z ( t+ ` R ) Y ) ) )
28 1 8 27 mp2b 
 |-  ( X = Z -> ( X R Y -> Z ( t+ ` R ) Y ) )