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\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2		cX	$$classX$$
3	1 0 2	cpred	$$classPred\left(R,A,X\right)$$
4	0	ccnv	$$class{R}^{-1}$$
5	2	csn	$$class\left\{X\right\}$$
6	4 5	cima	$$class{R}^{-1}\left[\left\{X\right\}\right]$$
7	1 6	cin	$$class\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
8	3 7	wceq	$$wffPred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$