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\in U$$
Assertion	dffrege99	$$⊢\left(\neg X\mathrm{t+}\left(R\right)Z\to Z=X\right)\leftrightarrow X\left(\mathrm{t+}\left(R\right)\cup \mathrm{I}\right)Z$$

Proof

Step	Hyp	Ref	Expression
1		frege99.z	$$⊢Z\in U$$
2		brun	$$⊢X\left(\mathrm{t+}\left(R\right)\cup \mathrm{I}\right)Z\leftrightarrow \left(X\mathrm{t+}\left(R\right)Z\vee X\mathrm{I}Z\right)$$
3		df-or	$$⊢\left(X\mathrm{t+}\left(R\right)Z\vee X\mathrm{I}Z\right)\leftrightarrow \left(\neg X\mathrm{t+}\left(R\right)Z\to X\mathrm{I}Z\right)$$
4	1	elexi	$$⊢Z\in \mathrm{V}$$
5	4	ideq	$$⊢X\mathrm{I}Z\leftrightarrow X=Z$$
6		eqcom	$$⊢X=Z\leftrightarrow Z=X$$
7	5 6	bitri	$$⊢X\mathrm{I}Z\leftrightarrow Z=X$$
8	7	imbi2i	$$⊢\left(\neg X\mathrm{t+}\left(R\right)Z\to X\mathrm{I}Z\right)\leftrightarrow \left(\neg X\mathrm{t+}\left(R\right)Z\to Z=X\right)$$
9	2 3 8	3bitrri	$$⊢\left(\neg X\mathrm{t+}\left(R\right)Z\to Z=X\right)\leftrightarrow X\left(\mathrm{t+}\left(R\right)\cup \mathrm{I}\right)Z$$