Metamath Proof Explorer


Theorem frege103

Description: Proposition 103 of Frege1879 p. 73. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege103.z 𝑍𝑉
Assertion frege103 ( ( 𝑍 = 𝑋𝑋 = 𝑍 ) → ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍𝑋 = 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 frege103.z 𝑍𝑉
2 1 frege100 ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍𝑍 = 𝑋 ) )
3 frege19 ( ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍𝑍 = 𝑋 ) ) → ( ( 𝑍 = 𝑋𝑋 = 𝑍 ) → ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍𝑋 = 𝑍 ) ) ) )
4 2 3 ax-mp ( ( 𝑍 = 𝑋𝑋 = 𝑍 ) → ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍𝑋 = 𝑍 ) ) )