Metamath Proof Explorer


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 ) 𝑍 )