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 e. U
Assertion	dffrege99	|- ( ( -. X ( t+ ` R ) Z -> Z = X ) <-> X ( ( t+ ` R ) u. _I ) Z )

Proof

Step	Hyp	Ref	Expression
1		frege99.z	|- Z e. U
2		brun	|- ( X ( ( t+ ` R ) u. _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 e. _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 ) u. _I ) Z )