Step |
Hyp |
Ref |
Expression |
1 |
|
frege99.z |
⊢ 𝑍 ∈ 𝑈 |
2 |
1
|
frege100 |
⊢ ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 = 𝑋 ) ) |
3 |
|
frege48 |
⊢ ( ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 = 𝑋 ) ) → ( ( 𝑍 = 𝑋 → ( 𝑍 𝑅 𝑉 → 𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) → ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → ( 𝑍 𝑅 𝑉 → 𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) → ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( 𝑍 𝑅 𝑉 → 𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) ) ) ) |
4 |
2 3
|
ax-mp |
⊢ ( ( 𝑍 = 𝑋 → ( 𝑍 𝑅 𝑉 → 𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) → ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → ( 𝑍 𝑅 𝑉 → 𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) → ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( 𝑍 𝑅 𝑉 → 𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) ) ) |