![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbeq2dv | Structured version Visualization version GIF version |
Description: Formula-building deduction rule 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 1992 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | csbeq2dv.1 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 1, 2 | csbeq2d 4134 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 ⦋csb 3674 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-sbc 3577 df-csb 3675 |
This theorem is referenced by: csbeq2i 4136 mpt2mptsx 7401 dmmpt2ssx 7403 fmpt2x 7404 el2mpt2csbcl 7418 offval22 7421 ovmptss 7426 fmpt2co 7428 mpt2sn 7436 mpt2curryd 7564 fvmpt2curryd 7566 cantnffval 8733 fsumcom2 14704 fsumcom2OLD 14705 fprodcom2 14913 fprodcom2OLD 14914 bpolylem 14978 bpolyval 14979 ruclem1 15159 natfval 16807 fucval 16819 evlfval 17058 mpfrcl 19720 pmatcollpw3lem 20790 fsumcn 22874 fsum2cn 22875 dvmptfsum 23937 ttgval 25954 msrfval 31741 poimirlem5 33727 poimirlem6 33728 poimirlem7 33729 poimirlem8 33730 poimirlem10 33732 poimirlem11 33733 poimirlem12 33734 poimirlem15 33737 poimirlem16 33738 poimirlem17 33739 poimirlem18 33740 poimirlem19 33741 poimirlem20 33742 poimirlem21 33743 poimirlem22 33744 poimirlem24 33746 poimirlem26 33748 poimirlem27 33749 cdleme31sde 36175 cdlemeg47rv2 36300 rnghmval 42401 dmmpt2ssx2 42625 |
Copyright terms: Public domain | W3C validator |