![]() |
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 3800 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) |
Ref | Expression |
---|---|
csbconstg | ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2932 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | 1 | csbconstgf 3800 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 ⦋csb 3788 |
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 1965 ax-8 2052 ax-9 2059 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-sbc 3684 df-csb 3789 |
This theorem is referenced by: csbconstgi 3803 csb0 4246 sbcel1g 4252 sbceq1g 4253 sbcel2 4254 sbceq2g 4255 csbidm 4267 2nreu 4277 csbopg 4696 sbcbr 4985 sbcbr12g 4986 sbcbr1g 4987 sbcbr2g 4988 csbmpt12 5297 csbmpt2 5298 sbcrel 5506 csbcnvgALT 5606 csbres 5699 csbrn 5901 sbcfung 6214 csbfv12 6545 csbfv2g 6546 elfvmptrab 6623 csbov 7020 csbov12g 7021 csbov1g 7022 csbov2g 7023 csbwrdg 13709 gsummptif1n0 18842 coe1fzgsumdlem 20175 evl1gsumdlem 20224 opsbc2ie 30024 disjpreima 30103 esum2dlem 30995 csbwrecsg 34050 csbrecsg 34051 csbrdgg 34052 csbmpo123 34054 f1omptsnlem 34059 relowlpssretop 34087 rdgeqoa 34093 csbfinxpg 34110 cdlemkid3N 37514 cdlemkid4 37515 cdlemk42 37522 brtrclfv2 39435 cotrclrcl 39450 frege77 39649 onfrALTlem5 40295 onfrALTlem4 40296 onfrALTlem5VD 40638 onfrALTlem4VD 40639 csbsngVD 40646 csbxpgVD 40647 csbresgVD 40648 csbrngVD 40649 csbfv12gALTVD 40652 disjinfi 40879 eubrdm 42677 iccelpart 42966 |
Copyright terms: Public domain | W3C validator |