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(XRY\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	$$⊢wRY\to w\mathrm{t+}\left(R\right)Y$$
6	5	sbcth	$$⊢X\in U\to \underset{\dot{}}{[}X/w\underset{\dot{}}{]}\left(wRY\to w\mathrm{t+}\left(R\right)Y\right)$$
7		frege53c	$$⊢\underset{\dot{}}{[}X/w\underset{\dot{}}{]}\left(wRY\to w\mathrm{t+}\left(R\right)Y\right)\to \left(X=Z\to \underset{\dot{}}{[}Z/w\underset{\dot{}}{]}\left(wRY\to w\mathrm{t+}\left(R\right)Y\right)\right)$$
8	6 7	syl	$$⊢X\in U\to \left(X=Z\to \underset{\dot{}}{[}Z/w\underset{\dot{}}{]}\left(wRY\to w\mathrm{t+}\left(R\right)Y\right)\right)$$
9		sbcim1	$$⊢\underset{\dot{}}{[}Z/w\underset{\dot{}}{]}\left(wRY\to w\mathrm{t+}\left(R\right)Y\right)\to \left(\underset{\dot{}}{[}Z/w\underset{\dot{}}{]}wRY\to \underset{\dot{}}{[}Z/w\underset{\dot{}}{]}w\mathrm{t+}\left(R\right)Y\right)$$
10	9	imim2i	$$⊢\left(X=Z\to \underset{\dot{}}{[}Z/w\underset{\dot{}}{]}\left(wRY\to w\mathrm{t+}\left(R\right)Y\right)\right)\to \left(X=Z\to \left(\underset{\dot{}}{[}Z/w\underset{\dot{}}{]}wRY\to \underset{\dot{}}{[}Z/w\underset{\dot{}}{]}w\mathrm{t+}\left(R\right)Y\right)\right)$$
11		dfsbcq	$$⊢X=Z\to \left(\underset{\dot{}}{[}X/w\underset{\dot{}}{]}wRY\leftrightarrow \underset{\dot{}}{[}Z/w\underset{\dot{}}{]}wRY\right)$$
12		sbcbr1g	$$⊢X\in U\to \left(\underset{\dot{}}{[}X/w\underset{\dot{}}{]}wRY\leftrightarrow ⦋X/w⦌wRY\right)$$
13		csbvarg	$$⊢X\in U\to ⦋X/w⦌w=X$$
14	13	breq1d	$$⊢X\in U\to \left(⦋X/w⦌wRY\leftrightarrow XRY\right)$$
15	12 14	bitrd	$$⊢X\in U\to \left(\underset{\dot{}}{[}X/w\underset{\dot{}}{]}wRY\leftrightarrow XRY\right)$$
16	1 15	ax-mp	$$⊢\underset{\dot{}}{[}X/w\underset{\dot{}}{]}wRY\leftrightarrow XRY$$
17	11 16	bitr3di	$$⊢X=Z\to \left(\underset{\dot{}}{[}Z/w\underset{\dot{}}{]}wRY\leftrightarrow XRY\right)$$
18		eqcom	$$⊢X=Z\leftrightarrow Z=X$$
19	18	biimpi	$$⊢X=Z\to Z=X$$
20	19 1	eqeltrdi	$$⊢X=Z\to Z\in U$$
21		sbcbr1g	$$⊢Z\in U\to \left(\underset{\dot{}}{[}Z/w\underset{\dot{}}{]}w\mathrm{t+}\left(R\right)Y\leftrightarrow ⦋Z/w⦌w\mathrm{t+}\left(R\right)Y\right)$$
22		csbvarg	$$⊢Z\in U\to ⦋Z/w⦌w=Z$$
23	22	breq1d	$$⊢Z\in U\to \left(⦋Z/w⦌w\mathrm{t+}\left(R\right)Y\leftrightarrow Z\mathrm{t+}\left(R\right)Y\right)$$
24	21 23	bitrd	$$⊢Z\in U\to \left(\underset{\dot{}}{[}Z/w\underset{\dot{}}{]}w\mathrm{t+}\left(R\right)Y\leftrightarrow Z\mathrm{t+}\left(R\right)Y\right)$$
25	20 24	syl	$$⊢X=Z\to \left(\underset{\dot{}}{[}Z/w\underset{\dot{}}{]}w\mathrm{t+}\left(R\right)Y\leftrightarrow Z\mathrm{t+}\left(R\right)Y\right)$$
26	17 25	imbi12d	$$⊢X=Z\to \left(\left(\underset{\dot{}}{[}Z/w\underset{\dot{}}{]}wRY\to \underset{\dot{}}{[}Z/w\underset{\dot{}}{]}w\mathrm{t+}\left(R\right)Y\right)\leftrightarrow \left(XRY\to Z\mathrm{t+}\left(R\right)Y\right)\right)$$
27	10 26	mpbidi	$$⊢\left(X=Z\to \underset{\dot{}}{[}Z/w\underset{\dot{}}{]}\left(wRY\to w\mathrm{t+}\left(R\right)Y\right)\right)\to \left(X=Z\to \left(XRY\to Z\mathrm{t+}\left(R\right)Y\right)\right)$$
28	1 8 27	mp2b	$$⊢X=Z\to \left(XRY\to Z\mathrm{t+}\left(R\right)Y\right)$$