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 U
frege91.y Y V
frege91.r R W
Assertion frege92 X = Z X R Y Z t+ R Y

Proof

Step Hyp Ref Expression
1 frege91.x X U
2 frege91.y Y V
3 frege91.r R W
4 vex w V
5 4 2 3 frege91 w R Y w t+ R Y
6 5 sbcth X 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 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 sbcbr1g X U [˙X / w]˙ w R Y X / w w R Y
12 csbvarg X U X / w w = X
13 12 breq1d X U X / w w R Y X R Y
14 11 13 bitrd X U [˙X / w]˙ w R Y X R Y
15 1 14 ax-mp [˙X / w]˙ w R Y X R Y
16 dfsbcq X = Z [˙X / w]˙ w R Y [˙Z / w]˙ w R Y
17 15 16 syl5rbbr 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 U
21 sbcbr1g Z U [˙Z / w]˙ w t+ R Y Z / w w t+ R Y
22 csbvarg Z U Z / w w = Z
23 22 breq1d Z U Z / w w t+ R Y Z t+ R Y
24 21 23 bitrd Z 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