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