Theorem csbconstg 3904

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3903 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 2979	. 2 ⊢ Ⅎ𝑥𝐵
2	1	csbconstgf 3903	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

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

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 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-sbc 3775  df-csb 3886

This theorem is referenced by:  csbconstgi  3906  csb0  4361  sbcel1g  4367  sbceq1g  4368  sbcel2  4369  sbceq2g  4370  csbidm  4384  2nreu  4395  csbopg  4823  sbcbr  5123  sbcbr12g  5124  sbcbr1g  5125  sbcbr2g  5126  csbmpt12  5446  csbmpt2  5447  sbcrel  5657  csbcnvgALT  5757  csbres  5858  csbrn  6062  sbcfung  6381  csbfv12  6715  csbfv2g  6716  elfvmptrab  6798  csbov  7201  csbov12g  7202  csbov1g  7203  csbov2g  7204  csbwrdg  13897  gsummptif1n0  19088  coe1fzgsumdlem  20471  evl1gsumdlem  20521  opsbc2ie  30241  disjpreima  30336  esum2dlem  31353  csbwrecsg  34610  csbrecsg  34611  csbrdgg  34612  csbmpo123  34614  f1omptsnlem  34619  relowlpssretop  34647  rdgeqoa  34653  csbfinxpg  34671  cdlemkid3N  38071  cdlemkid4  38072  cdlemk42  38079  brtrclfv2  40079  cotrclrcl  40094  frege77  40293  onfrALTlem5  40883  onfrALTlem4  40884  onfrALTlem5VD  41226  onfrALTlem4VD  41227  csbsngVD  41234  csbxpgVD  41235  csbresgVD  41236  csbrngVD  41237  csbfv12gALTVD  41240  disjinfi  41461  eubrdm  43278  iccelpart  43600