![]() |
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 1909 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | csbeq2dv.1 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 1, 2 | csbeq2d 3895 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ⦋csb 3889 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-12 2166 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-sbc 3774 df-csb 3890 |
This theorem is referenced by: csbeq2i 3897 csbeq12dv 3898 mpomptsx 8069 dmmpossx 8071 fmpox 8072 el2mpocsbcl 8090 offval22 8093 ovmptss 8098 fmpoco 8100 mposn 8108 mpocurryd 8275 fvmpocurryd 8277 cantnffval 9688 fsumcom2 15756 fprodcom2 15964 bpolylem 16028 bpolyval 16029 ruclem1 16211 natfval 17939 fucval 17952 evlfval 18212 rnghmval 20391 mpfrcl 22053 selvffval 22081 selvfval 22082 selvval 22083 pmatcollpw3lem 22729 fsumcn 24832 fsum2cn 24833 dvmptfsum 25951 mulsval 28059 precsexlemcbv 28154 ttgvalOLD 28752 msrfval 35278 poimirlem5 37229 poimirlem6 37230 poimirlem7 37231 poimirlem8 37232 poimirlem10 37234 poimirlem11 37235 poimirlem12 37236 poimirlem15 37239 poimirlem18 37242 poimirlem21 37245 poimirlem22 37246 poimirlem24 37248 poimirlem26 37250 poimirlem27 37251 cdleme31sde 39988 cdlemeg47rv2 40113 dmmpossx2 47586 |
Copyright terms: Public domain | W3C validator |