Metamath Proof Explorer


Theorem frege105

Description: Proposition 105 of Frege1879 p. 73. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege103.z ZV
Assertion frege105 ¬Xt+RZZ=XXt+RIZ

Proof

Step Hyp Ref Expression
1 frege103.z ZV
2 1 dffrege99 ¬Xt+RZZ=XXt+RIZ
3 frege52aid ¬Xt+RZZ=XXt+RIZ¬Xt+RZZ=XXt+RIZ
4 2 3 ax-mp ¬Xt+RZZ=XXt+RIZ