Theorem exse

Description: Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015)

	Ref	Expression
Assertion	exse	⊢ ( 𝐴 ∈ 𝑉 → 𝑅 Se 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rabexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
2	1	ralrimivw	⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
3		df-se	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
4	2 3	sylibr	⊢ ( 𝐴 ∈ 𝑉 → 𝑅 Se 𝐴 )