| 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 245 | . . 3 ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → (𝐴 = [𝑥]𝑅 → 𝜓)) |
| 5 | 4 | rexlimdva 3155 | . 2 ⊢ (𝜒 → (∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅 → 𝜓)) |
| 6 | elqsi 8810 | . . 3 ⊢ (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅) | |
| 7 | ectocl.1 | . . 3 ⊢ 𝑆 = (𝐵 / 𝑅) | |
| 8 | 6, 7 | eleq2s 2859 | . 2 ⊢ (𝐴 ∈ 𝑆 → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅) |
| 9 | 5, 8 | impel 505 | 1 ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∃wrex 3070 [cec 8743 / cqs 8744 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-qs 8751 |
| This theorem is referenced by: ectocl 8825 elqsn0 8826 qsdisj 8834 qsel 8836 eqgen 19199 orbsta 19331 sylow1lem3 19618 sylow2alem2 19636 sylow2a 19637 sylow2blem2 19639 frgpup1 19793 frgpup3lem 19795 quscrng 21293 pi1xfr 25088 pi1coghm 25094 vitalilem3 25645 qsdisjALTV 38616 eqvrelqsel 38617 |
| Copyright terms: Public domain | W3C validator |