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