![]() |
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 3569 | . 2 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ⦋csb 3566 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-sbc 3469 df-csb 3567 |
This theorem is referenced by: csbco3g 4033 csbidm 4035 fmptcof 6437 mpt2mptsx 7278 dmmpt2ssx 7280 fmpt2x 7281 ovmptss 7303 fmpt2co 7305 xpf1o 8163 hsmexlem2 9287 iundom2g 9400 sumeq2ii 14467 summolem3 14489 summolem2a 14490 summo 14492 zsum 14493 fsum 14495 sumsnf 14517 sumsn 14519 fsumcnv 14548 fsumcom2 14549 fsumcom2OLD 14550 fsumshftm 14557 fsum0diag2 14559 prodeq2ii 14687 prodmolem3 14707 prodmolem2a 14708 prodmo 14710 zprod 14711 fprod 14715 prodsn 14736 prodsnf 14738 fprodcnv 14757 fprodcom2 14758 fprodcom2OLD 14759 bpolylem 14823 bpolyval 14824 ruclem1 15004 pcmpt 15643 gsumvalx 17317 odfval 17998 odval 17999 telgsumfzslem 18431 telgsumfzs 18432 psrval 19410 psrass1lem 19425 mpfrcl 19566 evlsval 19567 evls1fval 19732 fsum2cn 22721 iunmbl2 23371 dvfsumlem1 23834 itgsubst 23857 q1pval 23958 r1pval 23961 rlimcnp2 24738 fsumdvdscom 24956 fsumdvdsmul 24966 ttgval 25800 fsumiunle 29703 msrfval 31560 poimirlem1 33540 poimirlem3 33542 poimirlem4 33543 poimirlem5 33544 poimirlem6 33545 poimirlem7 33546 poimirlem8 33547 poimirlem10 33549 poimirlem11 33550 poimirlem12 33551 poimirlem15 33554 poimirlem16 33555 poimirlem17 33556 poimirlem18 33557 poimirlem19 33558 poimirlem20 33559 poimirlem21 33560 poimirlem22 33561 poimirlem23 33562 poimirlem24 33563 poimirlem25 33564 poimirlem26 33565 poimirlem27 33566 poimirlem28 33567 cdleme31snd 35991 cdlemeg46c 36118 cdlemkid2 36529 cdlemk46 36553 cdlemk53b 36561 cdlemk53 36562 monotuz 37823 oddcomabszz 37826 fnwe2val 37936 fnwe2lem1 37937 fnwe2lem2 37938 mendval 38070 sumsnd 39499 climinf2mpt 40264 climinfmpt 40265 sge0f1o 40917 rnghmval 42216 dmmpt2ssx2 42440 |
Copyright terms: Public domain | W3C validator |