![]() |
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 8123 | . 2 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 [cec 8083 |
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 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2747 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-rab 3094 df-v 3414 df-dif 3831 df-un 3833 df-in 3835 df-ss 3842 df-nul 4178 df-if 4349 df-sn 4440 df-pr 4442 df-op 4446 df-br 4928 df-opab 4990 df-xp 5410 df-cnv 5412 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-ec 8087 |
This theorem is referenced by: brecop 8186 eroveu 8188 erov 8190 ecovcom 8199 ecovass 8200 ecovdi 8201 addsrmo 10289 mulsrmo 10290 addsrpr 10291 mulsrpr 10292 supsrlem 10327 supsr 10328 qus0 18115 qusinv 18116 qussub 18117 sylow2blem2 18501 frgpadd 18643 vrgpval 18647 vrgpinv 18649 frgpup3lem 18657 qusabl 18735 quscrng 19728 qustgplem 22426 pi1addval 23349 pi1xfrf 23354 pi1xfrval 23355 pi1xfrcnvlem 23357 pi1xfrcnv 23358 pi1cof 23360 pi1coval 23361 pi1coghm 23362 vitalilem3 23908 ismntoplly 30901 linedegen 33095 fvline 33096 |
Copyright terms: Public domain | W3C validator |