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 3502 | . 2 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ⦋csb 3499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-sbc 3403 df-csb 3500 |
This theorem is referenced by: csbco3g 3952 csbidm 3954 fmptcof 6304 mpt2mptsx 7122 dmmpt2ssx 7124 fmpt2x 7125 ovmptss 7145 fmpt2co 7147 xpf1o 8007 hsmexlem2 9132 iundom2g 9241 sumeq2ii 14271 summolem3 14292 summolem2a 14293 summo 14295 zsum 14296 fsum 14298 sumsn 14319 fsumcnv 14346 fsumcom2 14347 fsumcom2OLD 14348 fsumshftm 14355 fsum0diag2 14357 prodeq2ii 14482 prodmolem3 14502 prodmolem2a 14503 prodmo 14505 zprod 14506 fprod 14510 prodsn 14531 prodsnf 14533 fprodcnv 14552 fprodcom2 14553 fprodcom2OLD 14554 bpolylem 14618 bpolyval 14619 ruclem1 14799 pcmpt 15434 gsumvalx 17093 odfval 17775 odval 17776 telgsumfzslem 18208 telgsumfzs 18209 psrval 19183 psrass1lem 19198 mpfrcl 19339 evlsval 19340 evls1fval 19505 fsum2cn 22482 iunmbl2 23132 dvfsumlem1 23593 itgsubst 23616 q1pval 23717 r1pval 23720 rlimcnp2 24493 fsumdvdscom 24711 fsumdvdsmul 24721 ttgval 25555 msrfval 30688 poimirlem1 32580 poimirlem3 32582 poimirlem4 32583 poimirlem5 32584 poimirlem6 32585 poimirlem7 32586 poimirlem8 32587 poimirlem10 32589 poimirlem11 32590 poimirlem12 32591 poimirlem15 32594 poimirlem16 32595 poimirlem17 32596 poimirlem18 32597 poimirlem19 32598 poimirlem20 32599 poimirlem21 32600 poimirlem22 32601 poimirlem23 32602 poimirlem24 32603 poimirlem25 32604 poimirlem26 32605 poimirlem27 32606 poimirlem28 32607 fsumshftdOLD 33256 cdleme31snd 34692 cdlemeg46c 34819 cdlemkid2 35230 cdlemk46 35254 cdlemk53b 35262 cdlemk53 35263 monotuz 36524 oddcomabszz 36527 fnwe2val 36637 fnwe2lem1 36638 fnwe2lem2 36639 mendval 36772 sumsnd 38208 sumsnf 38636 sge0f1o 39275 rnghmval 41681 dmmpt2ssx2 41908 |
Copyright terms: Public domain | W3C validator |