![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbeq1d | Structured version Visualization version GIF version |
Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.) |
Ref | Expression |
---|---|
csbeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
csbeq1d | ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | csbeq1 3784 | . 2 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1508 ⦋csb 3781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-sbc 3677 df-csb 3782 |
This theorem is referenced by: csbco3g 4259 csbidm 4261 fmptcof 6714 mpomptsx 7569 dmmpossx 7571 fmpox 7572 ovmptss 7595 fmpoco 7597 xpf1o 8474 hsmexlem2 9646 iundom2g 9759 sumeq2ii 14909 summolem3 14930 summolem2a 14931 summo 14933 zsum 14934 fsum 14936 sumsnf 14958 fsumcnv 14987 fsumcom2 14988 fsumshftm 14995 fsum0diag2 14997 prodeq2ii 15126 prodmolem3 15146 prodmolem2a 15147 prodmo 15149 zprod 15150 fprod 15154 prodsn 15175 prodsnf 15177 fprodcnv 15196 fprodcom2 15197 bpolylem 15261 bpolyval 15262 ruclem1 15443 pcmpt 16083 gsumvalx 17751 odfval 18435 odfvalALT 18436 odval 18437 telgsumfzslem 18871 telgsumfzs 18872 psrval 19869 psrass1lem 19884 mpfrcl 20024 evlsval 20025 evls1fval 20201 fsum2cn 23198 iunmbl2 23877 dvfsumlem1 24342 itgsubst 24365 q1pval 24466 r1pval 24469 rlimcnp2 25262 fsumdvdscom 25480 fsumdvdsmul 25490 ttgval 26380 fsumiunle 30316 msrfval 32337 poimirlem1 34367 poimirlem3 34369 poimirlem4 34370 poimirlem5 34371 poimirlem6 34372 poimirlem7 34373 poimirlem8 34374 poimirlem10 34376 poimirlem11 34377 poimirlem12 34378 poimirlem15 34381 poimirlem16 34382 poimirlem17 34383 poimirlem18 34384 poimirlem19 34385 poimirlem20 34386 poimirlem21 34387 poimirlem22 34388 poimirlem23 34389 poimirlem24 34390 poimirlem25 34391 poimirlem26 34392 poimirlem27 34393 poimirlem28 34394 cdleme31snd 37000 cdlemeg46c 37127 cdlemkid2 37538 cdlemk46 37562 cdlemk53b 37570 cdlemk53 37571 monotuz 38968 oddcomabszz 38971 fnwe2val 39079 fnwe2lem1 39080 fnwe2lem2 39081 mendval 39213 sumsnd 40736 climinf2mpt 41456 climinfmpt 41457 sge0f1o 42125 rnghmval 43556 dmmpossx2 43779 |
Copyright terms: Public domain | W3C validator |