Theorem frege100

Description: One direction of dffrege99 . Proposition 100 of Frege1879 p. 72. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	frege99.z	⊢ 𝑍 ∈ 𝑈
Assertion	frege100	⊢ ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 = 𝑋 ) )

Proof

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