Metamath Proof Explorer

Theorem eqvrelqsel

Description: If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 28-Dec-2019)

Ref Expression
Assertion eqvrelqsel ⊢ EqvRel R ∧ B ∈ A / R ∧ C ∈ B → B = C R

Proof

Step Hyp Ref Expression
1 eqid ⊢ A / R = A / R
2 eleq2 ⊢ x R = B → C ∈ x R ↔ C ∈ B
3 eqeq1 ⊢ x R = B → x R = C R ↔ B = C R
4 2 3 imbi12d ⊢ x R = B → C ∈ x R → x R = C R ↔ C ∈ B → B = C R
5 elecALTV ⊢ x ∈ V ∧ C ∈ x R → C ∈ x R ↔ x R C
6 5 el2v1 ⊢ C ∈ x R → C ∈ x R ↔ x R C
7 6 ibi ⊢ C ∈ x R → x R C
8 simpll ⊢ EqvRel R ∧ x ∈ A ∧ x R C → EqvRel R
9 simpr ⊢ EqvRel R ∧ x ∈ A ∧ x R C → x R C
10 8 9 eqvrelthi ⊢ EqvRel R ∧ x ∈ A ∧ x R C → x R = C R
11 10 ex ⊢ EqvRel R ∧ x ∈ A → x R C → x R = C R
12 7 11 syl5 ⊢ EqvRel R ∧ x ∈ A → C ∈ x R → x R = C R
13 1 4 12 ectocld ⊢ EqvRel R ∧ B ∈ A / R → C ∈ B → B = C R
14 13 3impia ⊢ EqvRel R ∧ B ∈ A / R ∧ C ∈ B → B = C R