Theorem seex

Description: The R -preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014)

	Ref	Expression
Assertion	seex	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-se	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V )
2		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐵 ) )
3	2	rabbidv	⊢ ( 𝑦 = 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } = { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } )
4	3	eleq1d	⊢ ( 𝑦 = 𝐵 → ( { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V ↔ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V ) )
5	4	rspccva	⊢ ( ( ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V )
6	1 5	sylanb	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V )