Definition df-pred

Description: Define the predecessor class of a binary relation. This is the class of all elements y of A such that y R X (see elpred ). (Contributed by Scott Fenton, 29-Jan-2011)

	Ref	Expression
Assertion	df-pred	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1		cA	|- A
2		cX	|- X
3	1 0 2	cpred	|- Pred ( R , A , X )
4	0	ccnv	|- `' R
5	2	csn	|- { X }
6	4 5	cima	|- ( `' R " { X } )
7	1 6	cin	|- ( A i^i ( `' R " { X } ) )
8	3 7	wceq	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )