Theorem ecexg

Description: An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995)

	Ref	Expression
Assertion	ecexg	⊢ ( 𝑅 ∈ 𝐵 → [ 𝐴 ] 𝑅 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-ec	⊢ [ 𝐴 ] 𝑅 = ( 𝑅 “ { 𝐴 } )
2		imaexg	⊢ ( 𝑅 ∈ 𝐵 → ( 𝑅 “ { 𝐴 } ) ∈ V )
3	1 2	eqeltrid	⊢ ( 𝑅 ∈ 𝐵 → [ 𝐴 ] 𝑅 ∈ V )