Theorem erex

Description: An equivalence relation is a set if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010) (Proof shortened by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Assertion	erex	⊢ ( 𝑅 Er 𝐴 → ( 𝐴 ∈ 𝑉 → 𝑅 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		erssxp	⊢ ( 𝑅 Er 𝐴 → 𝑅 ⊆ ( 𝐴 × 𝐴 ) )
2		sqxpexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 𝐴 ) ∈ V )
3		ssexg	⊢ ( ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ∈ V ) → 𝑅 ∈ V )
4	1 2 3	syl2an	⊢ ( ( 𝑅 Er 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝑅 ∈ V )
5	4	ex	⊢ ( 𝑅 Er 𝐴 → ( 𝐴 ∈ 𝑉 → 𝑅 ∈ V ) )