Metamath Proof Explorer

Theorem qsel

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)

Ref Expression
Assertion qsel ⊢ R Er X ∧ 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 elecg ⊢ C ∈ x R ∧ x ∈ V → C ∈ x R ↔ x R C
6 5 elvd ⊢ C ∈ x R → C ∈ x R ↔ x R C
7 6 ibi ⊢ C ∈ x R → x R C
8 simpll ⊢ R Er X ∧ x ∈ A ∧ x R C → R Er X
9 simpr ⊢ R Er X ∧ x ∈ A ∧ x R C → x R C
10 8 9 erthi ⊢ R Er X ∧ x ∈ A ∧ x R C → x R = C R
11 10 ex ⊢ R Er X ∧ x ∈ A → x R C → x R = C R
12 7 11 syl5 ⊢ R Er X ∧ x ∈ A → C ∈ x R → x R = C R
13 1 4 12 ectocld ⊢ R Er X ∧ B ∈ A / R → C ∈ B → B = C R
14 13 3impia ⊢ R Er X ∧ B ∈ A / R ∧ C ∈ B → B = C R