Metamath Proof Explorer


Theorem dffrege99

Description: If Z is identical with X or follows X in the R -sequence, then we say : " Z belongs to the R -sequence beginning with X " or " X belongs to the R -sequence ending with Z ". Definition 99 of Frege1879 p. 71. (Contributed by RP, 2-Jul-2020)

Ref Expression
Hypothesis frege99.z Z U
Assertion dffrege99 ¬ X t+ R Z Z = X X t+ R I Z

Proof

Step Hyp Ref Expression
1 frege99.z Z U
2 brun X t+ R I Z X t+ R Z X I Z
3 df-or X t+ R Z X I Z ¬ X t+ R Z X I Z
4 1 elexi Z V
5 4 ideq X I Z X = Z
6 eqcom X = Z Z = X
7 5 6 bitri X I Z Z = X
8 7 imbi2i ¬ X t+ R Z X I Z ¬ X t+ R Z Z = X
9 2 3 8 3bitrri ¬ X t+ R Z Z = X X t+ R I Z