eqvrelqsel - Mathbox for Peter Mazsa

	Mathbox for Peter Mazsa		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > eqvrelqsel		Structured version Visualization version GIF version

Theorem eqvrelqsel 39137

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.)

**Assertion**
Ref	Expression
eqvrelqsel	⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅)

Proof of Theorem eqvrelqsel Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2752	. . 3 ⊢ (𝐴 / 𝑅) = (𝐴 / 𝑅)
2		eleq2 2841	. . . 4 ⊢ ([𝑥]𝑅 = 𝐵 → (𝐶 ∈ [𝑥]𝑅 ↔ 𝐶 ∈ 𝐵))
3		eqeq1 2756	. . . 4 ⊢ ([𝑥]𝑅 = 𝐵 → ([𝑥]𝑅 = [𝐶]𝑅 ↔ 𝐵 = [𝐶]𝑅))
4	2, 3	imbi12d 346	. . 3 ⊢ ([𝑥]𝑅 = 𝐵 → ((𝐶 ∈ [𝑥]𝑅 → [𝑥]𝑅 = [𝐶]𝑅) ↔ (𝐶 ∈ 𝐵 → 𝐵 = [𝐶]𝑅)))
5		elecALTV 38708	. . . . . 6 ⊢ ((𝑥 ∈ V ∧ 𝐶 ∈ [𝑥]𝑅) → (𝐶 ∈ [𝑥]𝑅 ↔ 𝑥𝑅𝐶))
6	5	el2v1 38666	. . . . 5 ⊢ (𝐶 ∈ [𝑥]𝑅 → (𝐶 ∈ [𝑥]𝑅 ↔ 𝑥𝑅𝐶))
7	6	ibi 269	. . . 4 ⊢ (𝐶 ∈ [𝑥]𝑅 → 𝑥𝑅𝐶)
8		simpll 774	. . . . . 6 ⊢ ((( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥𝑅𝐶) → EqvRel 𝑅)
9		simpr 487	. . . . . 6 ⊢ ((( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥𝑅𝐶) → 𝑥𝑅𝐶)
10	8, 9	eqvrelthi 39134	. . . . 5 ⊢ ((( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥𝑅𝐶) → [𝑥]𝑅 = [𝐶]𝑅)
11	10	ex 415	. . . 4 ⊢ (( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝑥𝑅𝐶 → [𝑥]𝑅 = [𝐶]𝑅))
12	7, 11	syl5 34	. . 3 ⊢ (( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝐶 ∈ [𝑥]𝑅 → [𝑥]𝑅 = [𝐶]𝑅))
13	1, 4, 12	ectocld 8748	. 2 ⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → (𝐶 ∈ 𝐵 → 𝐵 = [𝐶]𝑅))
14	13	3impia 1126	1 ⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1095 = wceq 1550 ∈ wcel 2132 Vcvv 3444 class class class wbr 5090 [cec 8660 / cqs 8661 EqvRel weqvrel 38637

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-ext 2724 ax-sep 5236 ax-pr 5380

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-sb 2081 df-clab 2731 df-cleq 2744 df-clel 2827 df-ne 2948 df-ral 3067 df-rex 3077 df-rab 3405 df-v 3446 df-dif 3898 df-un 3900 df-in 3902 df-ss 3912 df-nul 4277 df-if 4471 df-sn 4573 df-pr 4575 df-op 4579 df-br 5091 df-opab 5153 df-id 5531 df-xp 5642 df-rel 5643 df-cnv 5644 df-co 5645 df-dm 5646 df-rn 5647 df-res 5648 df-ima 5649 df-ec 8664 df-qs 8668 df-refrel 39029 df-symrel 39061 df-trrel 39095 df-eqvrel 39106

This theorem is referenced by: erimeq2 39200

W3C validator