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+ ‘ 𝑅 ) 𝑍 → 𝑋 = 𝑍 ) ) |
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+ ‘ 𝑅 ) 𝑍 → 𝑋 = 𝑍 ) ) |