Theorem setlikespec

Description: If R is set-like in A , then all predecessor classes of elements of A exist. (Contributed by Scott Fenton, 20-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	setlikespec	$$⊢\left(X\in A\wedge R\mathrm{Se}A\right)\to Pred\left(R,A,X\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{x\in A|xRX\right\}=\left\{x|\left(x\in A\wedge xRX\right)\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	elpred	$$⊢X\in A\to \left(x\in Pred\left(R,A,X\right)\leftrightarrow \left(x\in A\wedge xRX\right)\right)$$
4	3	abbi2dv	$$⊢X\in A\to Pred\left(R,A,X\right)=\left\{x|\left(x\in A\wedge xRX\right)\right\}$$
5	1 4	eqtr4id	$$⊢X\in A\to \left\{x\in A|xRX\right\}=Pred\left(R,A,X\right)$$
6	5	adantr	$$⊢\left(X\in A\wedge R\mathrm{Se}A\right)\to \left\{x\in A|xRX\right\}=Pred\left(R,A,X\right)$$
7		seex	$$⊢\left(R\mathrm{Se}A\wedge X\in A\right)\to \left\{x\in A|xRX\right\}\in \mathrm{V}$$
8	7	ancoms	$$⊢\left(X\in A\wedge R\mathrm{Se}A\right)\to \left\{x\in A|xRX\right\}\in \mathrm{V}$$
9	6 8	eqeltrrd	$$⊢\left(X\in A\wedge R\mathrm{Se}A\right)\to Pred\left(R,A,X\right)\in \mathrm{V}$$