Theorem trpred

Description: The class of predecessors of an element of a transitive class for the membership relation is that element. (Contributed by BJ, 12-Oct-2024)

	Ref	Expression
Assertion	trpred	$$⊢\left(\mathrm{Tr}A\wedge X\in A\right)\to Pred\left(\mathrm{E},A,X\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		predep	$$⊢X\in A\to Pred\left(\mathrm{E},A,X\right)=A\cap X$$
2	1	adantl	$$⊢\left(\mathrm{Tr}A\wedge X\in A\right)\to Pred\left(\mathrm{E},A,X\right)=A\cap X$$
3		trss	$$⊢\mathrm{Tr}A\to \left(X\in A\to X\subseteq A\right)$$
4	3	imp	$$⊢\left(\mathrm{Tr}A\wedge X\in A\right)\to X\subseteq A$$
5		sseqin2	$$⊢X\subseteq A\leftrightarrow A\cap X=X$$
6	4 5	sylib	$$⊢\left(\mathrm{Tr}A\wedge X\in A\right)\to A\cap X=X$$
7	2 6	eqtrd	$$⊢\left(\mathrm{Tr}A\wedge X\in A\right)\to Pred\left(\mathrm{E},A,X\right)=X$$