This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ecexg

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

Ref Expression
Assertion ecexg ⊢ R ∈ B → A R ∈ V

Proof

Step Hyp Ref Expression
1 df-ec ⊢ A R = R A
2 imaexg ⊢ R ∈ B → R A ∈ V
3 1 2 eqeltrid ⊢ R ∈ B → A R ∈ V