![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbconstg | Structured version Visualization version GIF version |
Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3578 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) |
Ref | Expression |
---|---|
csbconstg | ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2793 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | 1 | csbconstgf 3578 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ∈ wcel 2030 ⦋csb 3566 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-sbc 3469 df-csb 3567 |
This theorem is referenced by: csb0 4015 sbcel1g 4020 sbceq1g 4021 sbcel2 4022 sbceq2g 4023 csbidm 4035 csbopg 4451 sbcbr 4740 sbcbr12g 4741 sbcbr1g 4742 sbcbr2g 4743 csbmpt12 5039 csbmpt2 5040 sbcrel 5239 csbcnvgALT 5339 csbres 5431 csbrn 5631 sbcfung 5950 csbfv12 6269 csbfv2g 6270 elfvmptrab 6345 csbov 6728 csbov12g 6729 csbov1g 6730 csbov2g 6731 csbwrdg 13366 gsummptif1n0 18411 coe1fzgsumdlem 19719 evl1gsumdlem 19768 disjpreima 29523 esum2dlem 30282 csbwrecsg 33303 csbrecsg 33304 csbrdgg 33305 csbmpt22g 33307 f1omptsnlem 33313 relowlpssretop 33342 rdgeqoa 33348 csbfinxpg 33355 csbconstgi 34052 cdlemkid3N 36538 cdlemkid4 36539 cdlemk42 36546 brtrclfv2 38336 cotrclrcl 38351 frege77 38551 sbcel2gOLD 39072 onfrALTlem5 39074 onfrALTlem4 39075 csbresgOLD 39370 onfrALTlem5VD 39435 onfrALTlem4VD 39436 csbsngVD 39443 csbxpgVD 39444 csbresgVD 39445 csbrngVD 39446 csbfv12gALTVD 39449 disjinfi 39694 iccelpart 41694 |
Copyright terms: Public domain | W3C validator |