Theorem frege105

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

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

Proof

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