![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbeq2dv | Structured version Visualization version GIF version |
Description: Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
Ref | Expression |
---|---|
csbeq2dv.1 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbeq2dv | ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1873 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | csbeq2dv.1 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 1, 2 | csbeq2d 4253 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ⦋csb 3785 |
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-12 2104 ax-ext 2747 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2756 df-cleq 2768 df-clel 2843 df-sbc 3681 df-csb 3786 |
This theorem is referenced by: csbeq2i 4255 mpomptsx 7567 dmmpossx 7569 fmpox 7570 el2mpocsbcl 7585 offval22 7588 ovmptss 7593 fmpoco 7595 mposn 7603 mpocurryd 7735 fvmpocurryd 7737 cantnffval 8916 fsumcom2 14983 fprodcom2 15192 bpolylem 15256 bpolyval 15257 ruclem1 15438 natfval 17068 fucval 17080 evlfval 17319 mpfrcl 20005 pmatcollpw3lem 21089 fsumcn 23175 fsum2cn 23176 dvmptfsum 24269 ttgval 26358 msrfval 32274 poimirlem5 34316 poimirlem6 34317 poimirlem7 34318 poimirlem8 34319 poimirlem10 34321 poimirlem11 34322 poimirlem12 34323 poimirlem15 34326 poimirlem16 34327 poimirlem17 34328 poimirlem18 34329 poimirlem19 34330 poimirlem20 34331 poimirlem21 34332 poimirlem22 34333 poimirlem24 34335 poimirlem26 34337 poimirlem27 34338 cdleme31sde 36944 cdlemeg47rv2 37069 rnghmval 43500 dmmpt2ssx2 43723 |
Copyright terms: Public domain | W3C validator |