| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eceq1d | Structured version Visualization version GIF version | ||
| Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.) |
| Ref | Expression |
|---|---|
| eceq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| eceq1d | ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eceq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | eceq1 8722 | . 2 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) | |
| 3 | 1, 2 | syl 18 | 1 ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1563 [cec 8680 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-xp 5657 df-cnv 5659 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-ec 8684 |
| This theorem is referenced by: brecop 8796 eroveu 8798 erov 8800 ecovcom 8809 ecovass 8810 ecovdi 8811 addsrmo 11046 mulsrmo 11047 addsrpr 11048 mulsrpr 11049 supsrlem 11084 supsr 11085 qus0 19248 qusinv 19249 qussub 19250 sylow2blem2 19679 frgpadd 19821 vrgpval 19825 vrgpinv 19827 frgpup3lem 19835 qusabl 19923 quscrng 21382 pzriprnglem11 21598 pzriprnglem12 21599 qustgplem 24235 pi1addval 25164 pi1xfrf 25169 pi1xfrval 25170 pi1xfrcnvlem 25172 pi1xfrcnv 25173 pi1cof 25175 pi1coval 25176 pi1coghm 25177 vitalilem3 25726 elrlocbasi 33495 rlocaddval 33497 rlocmulval 33498 rloccring 33499 rloc0g 33500 rloc1r 33501 rlocf1 33502 rlocisunit 33504 idomsubr 33540 opprqusmulr 33685 zringfrac 33756 ismntoplly 34327 linedegen 36501 fvline 36502 aks5lem3a 42813 aks5lem5a 42815 aks5lem6 42816 |
| Copyright terms: Public domain | W3C validator |