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	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑋 ) }
2		vex	⊢ 𝑥 ∈ V
3	2	elpred	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑥 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑋 ) ) )
4	3	abbi2dv	⊢ ( 𝑋 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑋 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑋 ) } )
5	1 4	eqtr4id	⊢ ( 𝑋 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
6	5	adantr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
7		seex	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } ∈ V )
8	7	ancoms	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } ∈ V )
9	6 8	eqeltrrd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )