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 𝐴 ∧ 𝑋 ∈ 𝐴 ) → Pred ( E , 𝐴 , 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		predep	⊢ ( 𝑋 ∈ 𝐴 → Pred ( E , 𝐴 , 𝑋 ) = ( 𝐴 ∩ 𝑋 ) )
2	1	adantl	⊢ ( ( Tr 𝐴 ∧ 𝑋 ∈ 𝐴 ) → Pred ( E , 𝐴 , 𝑋 ) = ( 𝐴 ∩ 𝑋 ) )
3		trss	⊢ ( Tr 𝐴 → ( 𝑋 ∈ 𝐴 → 𝑋 ⊆ 𝐴 ) )
4	3	imp	⊢ ( ( Tr 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ⊆ 𝐴 )
5		sseqin2	⊢ ( 𝑋 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝑋 ) = 𝑋 )
6	4 5	sylib	⊢ ( ( Tr 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∩ 𝑋 ) = 𝑋 )
7	2 6	eqtrd	⊢ ( ( Tr 𝐴 ∧ 𝑋 ∈ 𝐴 ) → Pred ( E , 𝐴 , 𝑋 ) = 𝑋 )