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 ⊢ 𝑋 ∈ 𝑈
frege91.y ⊢ 𝑌 ∈ 𝑉
frege91.r ⊢ 𝑅 ∈ 𝑊
Assertion frege92 ( 𝑋 = 𝑍 → ( 𝑋 𝑅 𝑌 → 𝑍 ( t+ ‘ 𝑅 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 frege91.x ⊢ 𝑋 ∈ 𝑈
2 frege91.y ⊢ 𝑌 ∈ 𝑉
3 frege91.r ⊢ 𝑅 ∈ 𝑊
4 vex ⊢ 𝑤 ∈ V
5 4 2 3 frege91 ⊢ ( 𝑤 𝑅 𝑌 → 𝑤 ( t+ ‘ 𝑅 ) 𝑌 )
6 5 sbcth ⊢ ( 𝑋 ∈ 𝑈 → [ 𝑋 / 𝑤 ] ( 𝑤 𝑅 𝑌 → 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) )
7 frege53c ⊢ ( [ 𝑋 / 𝑤 ] ( 𝑤 𝑅 𝑌 → 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) → ( 𝑋 = 𝑍 → [ 𝑍 / 𝑤 ] ( 𝑤 𝑅 𝑌 → 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) ) )
8 6 7 syl ⊢ ( 𝑋 ∈ 𝑈 → ( 𝑋 = 𝑍 → [ 𝑍 / 𝑤 ] ( 𝑤 𝑅 𝑌 → 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) ) )
9 sbcim1 ⊢ ( [ 𝑍 / 𝑤 ] ( 𝑤 𝑅 𝑌 → 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) → ( [ 𝑍 / 𝑤 ] 𝑤 𝑅 𝑌 → [ 𝑍 / 𝑤 ] 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) )
10 9 imim2i ⊢ ( ( 𝑋 = 𝑍 → [ 𝑍 / 𝑤 ] ( 𝑤 𝑅 𝑌 → 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) ) → ( 𝑋 = 𝑍 → ( [ 𝑍 / 𝑤 ] 𝑤 𝑅 𝑌 → [ 𝑍 / 𝑤 ] 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) ) )
11 dfsbcq ⊢ ( 𝑋 = 𝑍 → ( [ 𝑋 / 𝑤 ] 𝑤 𝑅 𝑌 ↔ [ 𝑍 / 𝑤 ] 𝑤 𝑅 𝑌 ) )
12 sbcbr1g ⊢ ( 𝑋 ∈ 𝑈 → ( [ 𝑋 / 𝑤 ] 𝑤 𝑅 𝑌 ↔ ⦋ 𝑋 / 𝑤 ⦌ 𝑤 𝑅 𝑌 ) )
13 csbvarg ⊢ ( 𝑋 ∈ 𝑈 → ⦋ 𝑋 / 𝑤 ⦌ 𝑤 = 𝑋 )
14 13 breq1d ⊢ ( 𝑋 ∈ 𝑈 → ( ⦋ 𝑋 / 𝑤 ⦌ 𝑤 𝑅 𝑌 ↔ 𝑋 𝑅 𝑌 ) )
15 12 14 bitrd ⊢ ( 𝑋 ∈ 𝑈 → ( [ 𝑋 / 𝑤 ] 𝑤 𝑅 𝑌 ↔ 𝑋 𝑅 𝑌 ) )
16 1 15 ax-mp ⊢ ( [ 𝑋 / 𝑤 ] 𝑤 𝑅 𝑌 ↔ 𝑋 𝑅 𝑌 )
17 11 16 bitr3di ⊢ ( 𝑋 = 𝑍 → ( [ 𝑍 / 𝑤 ] 𝑤 𝑅 𝑌 ↔ 𝑋 𝑅 𝑌 ) )
18 eqcom ⊢ ( 𝑋 = 𝑍 ↔ 𝑍 = 𝑋 )
19 18 biimpi ⊢ ( 𝑋 = 𝑍 → 𝑍 = 𝑋 )
20 19 1 eqeltrdi ⊢ ( 𝑋 = 𝑍 → 𝑍 ∈ 𝑈 )
21 sbcbr1g ⊢ ( 𝑍 ∈ 𝑈 → ( [ 𝑍 / 𝑤 ] 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ↔ ⦋ 𝑍 / 𝑤 ⦌ 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) )
22 csbvarg ⊢ ( 𝑍 ∈ 𝑈 → ⦋ 𝑍 / 𝑤 ⦌ 𝑤 = 𝑍 )
23 22 breq1d ⊢ ( 𝑍 ∈ 𝑈 → ( ⦋ 𝑍 / 𝑤 ⦌ 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑍 ( t+ ‘ 𝑅 ) 𝑌 ) )
24 21 23 bitrd ⊢ ( 𝑍 ∈ 𝑈 → ( [ 𝑍 / 𝑤 ] 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑍 ( t+ ‘ 𝑅 ) 𝑌 ) )
25 20 24 syl ⊢ ( 𝑋 = 𝑍 → ( [ 𝑍 / 𝑤 ] 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑍 ( t+ ‘ 𝑅 ) 𝑌 ) )
26 17 25 imbi12d ⊢ ( 𝑋 = 𝑍 → ( ( [ 𝑍 / 𝑤 ] 𝑤 𝑅 𝑌 → [ 𝑍 / 𝑤 ] 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) ↔ ( 𝑋 𝑅 𝑌 → 𝑍 ( t+ ‘ 𝑅 ) 𝑌 ) ) )
27 10 26 mpbidi ⊢ ( ( 𝑋 = 𝑍 → [ 𝑍 / 𝑤 ] ( 𝑤 𝑅 𝑌 → 𝑤 ( t+ ‘ 𝑅 ) 𝑌 ) ) → ( 𝑋 = 𝑍 → ( 𝑋 𝑅 𝑌 → 𝑍 ( t+ ‘ 𝑅 ) 𝑌 ) ) )
28 1 8 27 mp2b ⊢ ( 𝑋 = 𝑍 → ( 𝑋 𝑅 𝑌 → 𝑍 ( t+ ‘ 𝑅 ) 𝑌 ) )