![]() |
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 1910 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | csbeq2dv.1 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 1, 2 | csbeq2d 3895 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ⦋csb 3889 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-12 2164 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-sbc 3775 df-csb 3890 |
This theorem is referenced by: csbeq2i 3897 csbeq12dv 3898 mpomptsx 8062 dmmpossx 8064 fmpox 8065 el2mpocsbcl 8084 offval22 8087 ovmptss 8092 fmpoco 8094 mposn 8102 mpocurryd 8268 fvmpocurryd 8270 cantnffval 9678 fsumcom2 15744 fprodcom2 15952 bpolylem 16016 bpolyval 16017 ruclem1 16199 natfval 17927 fucval 17940 evlfval 18200 rnghmval 20368 mpfrcl 22018 selvffval 22046 selvfval 22047 selvval 22048 pmatcollpw3lem 22672 fsumcn 24775 fsum2cn 24776 dvmptfsum 25894 mulsval 27996 precsexlemcbv 28091 ttgvalOLD 28667 msrfval 35083 poimirlem5 37033 poimirlem6 37034 poimirlem7 37035 poimirlem8 37036 poimirlem10 37038 poimirlem11 37039 poimirlem12 37040 poimirlem15 37043 poimirlem18 37046 poimirlem21 37049 poimirlem22 37050 poimirlem24 37052 poimirlem26 37054 poimirlem27 37055 cdleme31sde 39795 cdlemeg47rv2 39920 dmmpossx2 47323 |
Copyright terms: Public domain | W3C validator |