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	|- ( ( Tr A /\ X e. A ) -> Pred ( _E , A , X ) = X )

Proof

Step	Hyp	Ref	Expression
1		predep	|- ( X e. A -> Pred ( _E , A , X ) = ( A i^i X ) )
2	1	adantl	|- ( ( Tr A /\ X e. A ) -> Pred ( _E , A , X ) = ( A i^i X ) )
3		trss	|- ( Tr A -> ( X e. A -> X C_ A ) )
4	3	imp	|- ( ( Tr A /\ X e. A ) -> X C_ A )
5		sseqin2	|- ( X C_ A <-> ( A i^i X ) = X )
6	4 5	sylib	|- ( ( Tr A /\ X e. A ) -> ( A i^i X ) = X )
7	2 6	eqtrd	|- ( ( Tr A /\ X e. A ) -> Pred ( _E , A , X ) = X )