Theorem predasetex

Description: The predecessor class exists when A does. (Contributed by Scott Fenton, 8-Feb-2011)

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

Proof

Step	Hyp	Ref	Expression
1		predasetex.1	|- A e. _V
2		df-pred	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
3	1	inex1	|- ( A i^i ( `' R " { X } ) ) e. _V
4	2 3	eqeltri	|- Pred ( R , A , X ) e. _V