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 3511 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) |
Ref | Expression |
---|---|
csbconstg | ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | 1 | csbconstgf 3511 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ⦋csb 3499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-sbc 3403 df-csb 3500 |
This theorem is referenced by: csb0 3934 sbcel1g 3939 sbceq1g 3940 sbcel2 3941 sbceq2g 3942 csbidm 3954 csbopg 4358 sbcbr 4637 sbcbr12g 4638 sbcbr1g 4639 sbcbr2g 4640 csbmpt12 4934 csbmpt2 4935 sbcrel 5128 csbcnvgALT 5229 csbres 5320 csbrn 5514 sbcfung 5827 csbfv12 6141 csbfv2g 6142 elfvmptrab 6214 csbov 6586 csbov12g 6587 csbov1g 6588 csbov2g 6589 csbwrdg 13189 gsummptif1n0 18188 coe1fzgsumdlem 19492 evl1gsumdlem 19541 rusgrasn 26472 disjpreima 28779 esum2dlem 29481 csbwrecsg 32349 csbrecsg 32350 csbrdgg 32351 csbmpt22g 32353 f1omptsnlem 32359 relowlpssretop 32388 rdgeqoa 32394 csbfinxpg 32401 csbconstgi 33092 cdlemkid3N 35239 cdlemkid4 35240 cdlemk42 35247 brtrclfv2 37038 cotrclrcl 37053 frege77 37254 sbcel2gOLD 37776 onfrALTlem5 37778 onfrALTlem4 37779 csbfv12gALTOLD 38074 csbresgOLD 38077 onfrALTlem5VD 38143 onfrALTlem4VD 38144 csbsngVD 38151 csbxpgVD 38152 csbresgVD 38153 csbrngVD 38154 csbfv12gALTVD 38157 disjinfi 38375 iccelpart 39971 |
Copyright terms: Public domain | W3C validator |