Theorem setlikespec

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

	Ref	Expression
Assertion	setlikespec	|- ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. A | x R X } = { x | ( x e. A /\ x R X ) }
2		vex	|- x e. _V
3	2	elpred	|- ( X e. A -> ( x e. Pred ( R , A , X ) <-> ( x e. A /\ x R X ) ) )
4	3	abbi2dv	|- ( X e. A -> Pred ( R , A , X ) = { x | ( x e. A /\ x R X ) } )
5	1 4	eqtr4id	|- ( X e. A -> { x e. A | x R X } = Pred ( R , A , X ) )
6	5	adantr	|- ( ( X e. A /\ R Se A ) -> { x e. A | x R X } = Pred ( R , A , X ) )
7		seex	|- ( ( R Se A /\ X e. A ) -> { x e. A | x R X } e. _V )
8	7	ancoms	|- ( ( X e. A /\ R Se A ) -> { x e. A | x R X } e. _V )
9	6 8	eqeltrrd	|- ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )