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 38980

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 2737	. . 3 ⊢ (𝐴 / 𝑅) = (𝐴 / 𝑅)
2		eleq2 2826	. . . 4 ⊢ ([𝑥]𝑅 = 𝐵 → (𝐶 ∈ [𝑥]𝑅 ↔ 𝐶 ∈ 𝐵))
3		eqeq1 2741	. . . 4 ⊢ ([𝑥]𝑅 = 𝐵 → ([𝑥]𝑅 = [𝐶]𝑅 ↔ 𝐵 = [𝐶]𝑅))
4	2, 3	imbi12d 344	. . 3 ⊢ ([𝑥]𝑅 = 𝐵 → ((𝐶 ∈ [𝑥]𝑅 → [𝑥]𝑅 = [𝐶]𝑅) ↔ (𝐶 ∈ 𝐵 → 𝐵 = [𝐶]𝑅)))
5		elecALTV 38551	. . . . . 6 ⊢ ((𝑥 ∈ V ∧ 𝐶 ∈ [𝑥]𝑅) → (𝐶 ∈ [𝑥]𝑅 ↔ 𝑥𝑅𝐶))
6	5	el2v1 38509	. . . . 5 ⊢ (𝐶 ∈ [𝑥]𝑅 → (𝐶 ∈ [𝑥]𝑅 ↔ 𝑥𝑅𝐶))
7	6	ibi 267	. . . 4 ⊢ (𝐶 ∈ [𝑥]𝑅 → 𝑥𝑅𝐶)
8		simpll 767	. . . . . 6 ⊢ ((( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥𝑅𝐶) → EqvRel 𝑅)
9		simpr 484	. . . . . 6 ⊢ ((( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥𝑅𝐶) → 𝑥𝑅𝐶)
10	8, 9	eqvrelthi 38977	. . . . 5 ⊢ ((( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥𝑅𝐶) → [𝑥]𝑅 = [𝐶]𝑅)
11	10	ex 412	. . . 4 ⊢ (( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝑥𝑅𝐶 → [𝑥]𝑅 = [𝐶]𝑅))
12	7, 11	syl5 34	. . 3 ⊢ (( EqvRel 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝐶 ∈ [𝑥]𝑅 → [𝑥]𝑅 = [𝐶]𝑅))
13	1, 4, 12	ectocld 8733	. 2 ⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → (𝐶 ∈ 𝐵 → 𝐵 = [𝐶]𝑅))
14	13	3impia 1118	1 ⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 Vcvv 3442 class class class wbr 5100 [cec 8645 / cqs 8646 EqvRel weqvrel 38480

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5245 ax-pr 5381

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163 df-id 5529 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-ec 8649 df-qs 8653 df-refrel 38872 df-symrel 38904 df-trrel 38938 df-eqvrel 38949

This theorem is referenced by: erimeq2 39043

W3C validator