Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter III Member of sequence
frege104
Metamath Proof Explorer
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
⊢ Z ∈ V
Assertion
frege104
⊢ X t+ ⁡ R ∪ I Z → ¬ X t+ ⁡ R Z → X = Z
Proof
Step
Hyp
Ref
Expression
1
frege103.z
⊢ Z ∈ V
2
1
elexi
⊢ Z ∈ V
3
eqeq1
⊢ z = Z → z = X ↔ Z = X
4
eqeq2
⊢ z = Z → X = z ↔ X = Z
5
3 4
imbi12d
⊢ z = Z → z = X → X = z ↔ Z = X → X = Z
6
frege55c
⊢ z = X → X = z
7
2 5 6
vtocl
⊢ Z = X → X = Z
8
1
frege103
⊢ Z = X → X = Z → X t+ ⁡ R ∪ I Z → ¬ X t+ ⁡ R Z → X = Z
9
7 8
ax-mp
⊢ X t+ ⁡ R ∪ I Z → ¬ X t+ ⁡ R Z → X = Z