Theorem csbconstg 3902

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3901 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)

Assertion

Ref	Expression
csbconstg	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Distinct variable group:   𝑥,𝐵

Allowed substitution hints:   𝐴(𝑥)   𝑉(𝑥)

Proof of Theorem csbconstg

Step	Hyp	Ref	Expression
1		nfcv 2977	. 2 ⊢ Ⅎ𝑥𝐵
2	1	csbconstgf 3901	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ⦋csb 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sbc 3773  df-csb 3884

This theorem is referenced by:  csbconstgi  3904  csb0  4359  sbcel1g  4365  sbceq1g  4366  sbcel2  4367  sbceq2g  4368  csbidm  4382  2nreu  4393  csbopg  4821  sbcbr  5121  sbcbr12g  5122  sbcbr1g  5123  sbcbr2g  5124  csbmpt12  5444  csbmpt2  5445  sbcrel  5655  csbcnvgALT  5755  csbres  5856  csbrn  6060  sbcfung  6379  csbfv12  6713  csbfv2g  6714  elfvmptrab  6796  csbov  7199  csbov12g  7200  csbov1g  7201  csbov2g  7202  csbwrdg  13895  gsummptif1n0  19086  coe1fzgsumdlem  20469  evl1gsumdlem  20519  opsbc2ie  30239  disjpreima  30334  esum2dlem  31351  csbwrecsg  34611  csbrecsg  34612  csbrdgg  34613  csbmpo123  34615  f1omptsnlem  34620  relowlpssretop  34648  rdgeqoa  34654  csbfinxpg  34672  cdlemkid3N  38084  cdlemkid4  38085  cdlemk42  38092  brtrclfv2  40092  cotrclrcl  40107  frege77  40306  onfrALTlem5  40896  onfrALTlem4  40897  onfrALTlem5VD  41239  onfrALTlem4VD  41240  csbsngVD  41247  csbxpgVD  41248  csbresgVD  41249  csbrngVD  41250  csbfv12gALTVD  41253  disjinfi  41474  eubrdm  43291  iccelpart  43613