Theorem predep

Description: The predecessor under the membership relation is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	predep	|- ( X e. B -> Pred ( _E , A , X ) = ( A i^i X ) )

Proof

Step	Hyp	Ref	Expression
1		df-pred	|- Pred ( _E , A , X ) = ( A i^i ( `' _E " { X } ) )
2		relcnv	|- Rel `' _E
3		relimasn	|- ( Rel `' _E -> ( `' _E " { X } ) = { y | X `' _E y } )
4	2 3	ax-mp	|- ( `' _E " { X } ) = { y | X `' _E y }
5		brcnvg	|- ( ( X e. B /\ y e. _V ) -> ( X `' _E y <-> y _E X ) )
6	5	elvd	|- ( X e. B -> ( X `' _E y <-> y _E X ) )
7		epelg	|- ( X e. B -> ( y _E X <-> y e. X ) )
8	6 7	bitrd	|- ( X e. B -> ( X `' _E y <-> y e. X ) )
9	8	abbi1dv	|- ( X e. B -> { y | X `' _E y } = X )
10	4 9	syl5eq	|- ( X e. B -> ( `' _E " { X } ) = X )
11	10	ineq2d	|- ( X e. B -> ( A i^i ( `' _E " { X } ) ) = ( A i^i X ) )
12	1 11	syl5eq	|- ( X e. B -> Pred ( _E , A , X ) = ( A i^i X ) )