Theorem ecexr

Description: A nonempty equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐴 ∈ ( 𝑅 “ { 𝐵 } ) → ¬ ( 𝑅 “ { 𝐵 } ) = ∅ )
2		snprc	⊢ ( ¬ 𝐵 ∈ V ↔ { 𝐵 } = ∅ )
3		imaeq2	⊢ ( { 𝐵 } = ∅ → ( 𝑅 “ { 𝐵 } ) = ( 𝑅 “ ∅ ) )
4	2 3	sylbi	⊢ ( ¬ 𝐵 ∈ V → ( 𝑅 “ { 𝐵 } ) = ( 𝑅 “ ∅ ) )
5		ima0	⊢ ( 𝑅 “ ∅ ) = ∅
6	4 5	eqtrdi	⊢ ( ¬ 𝐵 ∈ V → ( 𝑅 “ { 𝐵 } ) = ∅ )
7	1 6	nsyl2	⊢ ( 𝐴 ∈ ( 𝑅 “ { 𝐵 } ) → 𝐵 ∈ V )
8		df-ec	⊢ [ 𝐵 ] 𝑅 = ( 𝑅 “ { 𝐵 } )
9	7 8	eleq2s	⊢ ( 𝐴 ∈ [ 𝐵 ] 𝑅 → 𝐵 ∈ V )