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

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 𝑅 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐵 = [ 𝐶 ] 𝑅 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝐴 / 𝑅 ) = ( 𝐴 / 𝑅 )
2 eleq2 ⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( 𝐶 ∈ [ 𝑥 ] 𝑅 ↔ 𝐶 ∈ 𝐵 ) )
3 eqeq1 ⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 ↔ 𝐵 = [ 𝐶 ] 𝑅 ) )
4 2 3 imbi12d ⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( ( 𝐶 ∈ [ 𝑥 ] 𝑅 → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 ) ↔ ( 𝐶 ∈ 𝐵 → 𝐵 = [ 𝐶 ] 𝑅 ) ) )
5 elecALTV ⊢ ( ( 𝑥 ∈ V ∧ 𝐶 ∈ [ 𝑥 ] 𝑅 ) → ( 𝐶 ∈ [ 𝑥 ] 𝑅 ↔ 𝑥 𝑅 𝐶 ) )
6 5 el2v1 ⊢ ( 𝐶 ∈ [ 𝑥 ] 𝑅 → ( 𝐶 ∈ [ 𝑥 ] 𝑅 ↔ 𝑥 𝑅 𝐶 ) )
7 6 ibi ⊢ ( 𝐶 ∈ [ 𝑥 ] 𝑅 → 𝑥 𝑅 𝐶 )
8 simpll ⊢ ( ( ( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝐶 ) → EqvRel 𝑅 )
9 simpr ⊢ ( ( ( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝐶 ) → 𝑥 𝑅 𝐶 )
10 8 9 eqvrelthi ⊢ ( ( ( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝐶 ) → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 )
11 10 ex ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑅 𝐶 → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 ) )
12 7 11 syl5 ⊢ ( ( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ∈ [ 𝑥 ] 𝑅 → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 ) )
13 1 4 12 ectocld ⊢ ( ( EqvRel 𝑅 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ) → ( 𝐶 ∈ 𝐵 → 𝐵 = [ 𝐶 ] 𝑅 ) )
14 13 3impia ⊢ ( ( EqvRel 𝑅 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐵 = [ 𝐶 ] 𝑅 )