Metamath Proof Explorer

Theorem ecelqsw

Description: Membership of an equivalence class in a quotient set. More restrictive antecedent; kept for backward compatibility; for new work, prefer ecelqs . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 9-Jul-2014) (Proof shortened by AV, 25-Nov-2025)

Ref Expression
Assertion ecelqsw ⊢ R ∈ V ∧ B ∈ A → B R ∈ A / R

Proof

Step Hyp Ref Expression
1 resexg ⊢ R ∈ V → R ↾ A ∈ V
2 ecelqs ⊢ R ↾ A ∈ V ∧ B ∈ A → B R ∈ A / R
3 1 2 sylan ⊢ R ∈ V ∧ B ∈ A → B R ∈ A / R