# 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}\in {U}$
frege91.y ${⊢}{Y}\in {V}$
frege91.r ${⊢}{R}\in {W}$
Assertion frege92 ${⊢}{X}={Z}\to \left({X}{R}{Y}\to {Z}\mathrm{t+}\left({R}\right){Y}\right)$

### Proof

Step Hyp Ref Expression
1 frege91.x ${⊢}{X}\in {U}$
2 frege91.y ${⊢}{Y}\in {V}$
3 frege91.r ${⊢}{R}\in {W}$
4 vex ${⊢}{w}\in \mathrm{V}$
5 4 2 3 frege91 ${⊢}{w}{R}{Y}\to {w}\mathrm{t+}\left({R}\right){Y}$
6 5 sbcth
7 frege53c
8 6 7 syl
9 sbcim1
10 9 imim2i
11 sbcbr1g
12 csbvarg
13 12 breq1d
14 11 13 bitrd
15 1 14 ax-mp
16 dfsbcq
17 15 16 syl5rbbr
18 eqcom ${⊢}{X}={Z}↔{Z}={X}$
19 18 biimpi ${⊢}{X}={Z}\to {Z}={X}$
20 19 1 eqeltrdi ${⊢}{X}={Z}\to {Z}\in {U}$
21 sbcbr1g
22 csbvarg
23 22 breq1d
24 21 23 bitrd
25 20 24 syl
26 17 25 imbi12d
27 10 26 mpbidi
28 1 8 27 mp2b ${⊢}{X}={Z}\to \left({X}{R}{Y}\to {Z}\mathrm{t+}\left({R}\right){Y}\right)$