![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ectocld | Structured version Visualization version GIF version |
Description: Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.) |
Ref | Expression |
---|---|
ectocl.1 | ⊢ 𝑆 = (𝐵 / 𝑅) |
ectocl.2 | ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) |
ectocld.3 | ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) |
Ref | Expression |
---|---|
ectocld | ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ectocld.3 | . . . 4 ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) | |
2 | ectocl.2 | . . . . 5 ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | eqcoms 2745 | . . . 4 ⊢ (𝐴 = [𝑥]𝑅 → (𝜑 ↔ 𝜓)) |
4 | 1, 3 | syl5ibcom 244 | . . 3 ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → (𝐴 = [𝑥]𝑅 → 𝜓)) |
5 | 4 | rexlimdva 3153 | . 2 ⊢ (𝜒 → (∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅 → 𝜓)) |
6 | elqsi 8710 | . . 3 ⊢ (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅) | |
7 | ectocl.1 | . . 3 ⊢ 𝑆 = (𝐵 / 𝑅) | |
8 | 6, 7 | eleq2s 2856 | . 2 ⊢ (𝐴 ∈ 𝑆 → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅) |
9 | 5, 8 | impel 507 | 1 ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃wrex 3074 [cec 8647 / cqs 8648 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rex 3075 df-qs 8655 |
This theorem is referenced by: ectocl 8725 elqsn0 8726 qsdisj 8734 qsel 8736 eqgen 18984 orbsta 19094 sylow1lem3 19383 sylow2alem2 19401 sylow2a 19402 sylow2blem2 19404 frgpup1 19558 frgpup3lem 19560 quscrng 20713 pi1xfr 24421 pi1coghm 24427 vitalilem3 24977 qsdisjALTV 37080 eqvrelqsel 37081 |
Copyright terms: Public domain | W3C validator |