Theorem predep

Description: The predecessor under the membership relation is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	predep	$$⊢X\in B\to Pred\left(\mathrm{E},A,X\right)=A\cap X$$

Proof

Step	Hyp	Ref	Expression
1		df-pred	$$⊢Pred\left(\mathrm{E},A,X\right)=A\cap {\mathrm{E}}^{-1}\left[\left\{X\right\}\right]$$
2		relcnv	$$⊢\mathrm{Rel}{\mathrm{E}}^{-1}$$
3		relimasn	$$⊢\mathrm{Rel}{\mathrm{E}}^{-1}\to {\mathrm{E}}^{-1}\left[\left\{X\right\}\right]=\left\{y|X{\mathrm{E}}^{-1}y\right\}$$
4	2 3	ax-mp	$$⊢{\mathrm{E}}^{-1}\left[\left\{X\right\}\right]=\left\{y|X{\mathrm{E}}^{-1}y\right\}$$
5		brcnvg	$$⊢\left(X\in B\wedge y\in \mathrm{V}\right)\to \left(X{\mathrm{E}}^{-1}y\leftrightarrow y\mathrm{E}X\right)$$
6	5	elvd	$$⊢X\in B\to \left(X{\mathrm{E}}^{-1}y\leftrightarrow y\mathrm{E}X\right)$$
7		epelg	$$⊢X\in B\to \left(y\mathrm{E}X\leftrightarrow y\in X\right)$$
8	6 7	bitrd	$$⊢X\in B\to \left(X{\mathrm{E}}^{-1}y\leftrightarrow y\in X\right)$$
9	8	abbi1dv	$$⊢X\in B\to \left\{y|X{\mathrm{E}}^{-1}y\right\}=X$$
10	4 9	syl5eq	$$⊢X\in B\to {\mathrm{E}}^{-1}\left[\left\{X\right\}\right]=X$$
11	10	ineq2d	$$⊢X\in B\to A\cap {\mathrm{E}}^{-1}\left[\left\{X\right\}\right]=A\cap X$$
12	1 11	syl5eq	$$⊢X\in B\to Pred\left(\mathrm{E},A,X\right)=A\cap X$$