Theorem csbconstg 3801

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.)

Assertion

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

Distinct variable group:   𝑥,𝐵

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

Proof of Theorem csbconstg

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

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