Theorem elpredim

Description: Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012)

	Ref	Expression
Hypothesis	elpredim.1	|- X e. _V
Assertion	elpredim	|- ( Y e. Pred ( R , A , X ) -> Y R X )

Proof

Step	Hyp	Ref	Expression
1		elpredim.1	|- X 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		elimasng	|- ( ( X e. _V /\ Y e. ( `' R " { X } ) ) -> ( Y e. ( `' R " { X } ) <-> <. X , Y >. e. `' R ) )
5		opelcnvg	|- ( ( X e. _V /\ Y e. ( `' R " { X } ) ) -> ( <. X , Y >. e. `' R <-> <. Y , X >. e. R ) )
6	4 5	bitrd	|- ( ( X e. _V /\ Y e. ( `' R " { X } ) ) -> ( Y e. ( `' R " { X } ) <-> <. Y , X >. e. R ) )
7	1 6	mpan	|- ( Y e. ( `' R " { X } ) -> ( Y e. ( `' R " { X } ) <-> <. Y , X >. e. R ) )
8	7	ibi	|- ( Y e. ( `' R " { X } ) -> <. Y , X >. e. R )
9		df-br	|- ( Y R X <-> <. Y , X >. e. R )
10	8 9	sylibr	|- ( Y e. ( `' R " { X } ) -> Y R X )
11	3 10	simplbiim	|- ( Y e. Pred ( R , A , X ) -> Y R X )