Theorem exse2

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

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) }
2		vex	⊢ 𝑦 ∈ V
3		vex	⊢ 𝑥 ∈ V
4	2 3	breldm	⊢ ( 𝑦 𝑅 𝑥 → 𝑦 ∈ dom 𝑅 )
5	4	adantl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 ∈ dom 𝑅 )
6	5	abssi	⊢ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) } ⊆ dom 𝑅
7	1 6	eqsstri	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ⊆ dom 𝑅
8		dmexg	⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
9		ssexg	⊢ ( ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ⊆ dom 𝑅 ∧ dom 𝑅 ∈ V ) → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
10	7 8 9	sylancr	⊢ ( 𝑅 ∈ 𝑉 → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
11	10	ralrimivw	⊢ ( 𝑅 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
12		df-se	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
13	11 12	sylibr	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 Se 𝐴 )