Theorem elpred

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011)

	Ref	Expression
Hypothesis	elpred.1	|- Y e. _V
Assertion	elpred	|- ( X e. D -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) )

Proof

Step	Hyp	Ref	Expression
1		elpred.1	|- Y e. _V
2		df-pred	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
3	2	elin2	|- ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y e. ( `' R " { X } ) ) )
4	1	eliniseg	|- ( X e. D -> ( Y e. ( `' R " { X } ) <-> Y R X ) )
5	4	anbi2d	|- ( X e. D -> ( ( Y e. A /\ Y e. ( `' R " { X } ) ) <-> ( Y e. A /\ Y R X ) ) )
6	3 5	syl5bb	|- ( X e. D -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) )