Metamath Proof Explorer


Theorem frege104

Description: Proposition 104 of Frege1879 p. 73.

Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collectionFrom Frege to Goedel, this proof has the minor clause and result swapped. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 frege103.z 𝑍𝑉
2 1 elexi 𝑍 ∈ V
3 eqeq1 ( 𝑧 = 𝑍 → ( 𝑧 = 𝑋𝑍 = 𝑋 ) )
4 eqeq2 ( 𝑧 = 𝑍 → ( 𝑋 = 𝑧𝑋 = 𝑍 ) )
5 3 4 imbi12d ( 𝑧 = 𝑍 → ( ( 𝑧 = 𝑋𝑋 = 𝑧 ) ↔ ( 𝑍 = 𝑋𝑋 = 𝑍 ) ) )
6 frege55c ( 𝑧 = 𝑋𝑋 = 𝑧 )
7 2 5 6 vtocl ( 𝑍 = 𝑋𝑋 = 𝑍 )
8 1 frege103 ( ( 𝑍 = 𝑋𝑋 = 𝑍 ) → ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍𝑋 = 𝑍 ) ) )
9 7 8 ax-mp ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍𝑋 = 𝑍 ) )