Metamath Proof Explorer


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 )