![]() |
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 2780 | . . . 4 ⊢ (𝐴 = [𝑥]𝑅 → (𝜑 ↔ 𝜓)) |
4 | 1, 3 | syl5ibcom 237 | . . 3 ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → (𝐴 = [𝑥]𝑅 → 𝜓)) |
5 | 4 | rexlimdva 3223 | . 2 ⊢ (𝜒 → (∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅 → 𝜓)) |
6 | elqsi 8148 | . . 3 ⊢ (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅) | |
7 | ectocl.1 | . . 3 ⊢ 𝑆 = (𝐵 / 𝑅) | |
8 | 6, 7 | eleq2s 2878 | . 2 ⊢ (𝐴 ∈ 𝑆 → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅) |
9 | 5, 8 | impel 498 | 1 ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ∃wrex 3083 [cec 8085 / cqs 8086 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-qs 8093 |
This theorem is referenced by: ectocl 8163 elqsn0 8164 qsdisj 8172 qsel 8174 eqgen 18128 orbsta 18226 sylow1lem3 18498 sylow2alem2 18516 sylow2a 18517 sylow2blem2 18519 frgpup1 18673 frgpup3lem 18675 quscrng 19746 pi1xfr 23374 pi1coghm 23380 vitalilem3 23926 qsdisjALTV 35324 eqvrelqsel 35325 |
Copyright terms: Public domain | W3C validator |