Theorem csbconstg 3512

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

Assertion

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

Distinct variable group:   𝑥,𝐵

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

Proof of Theorem csbconstg

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

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  4353  sbcbr  4632  sbcbr12g  4633  sbcbr1g  4634  sbcbr2g  4635  csbmpt12  4924  csbmpt2  4925  sbcrel  5118  csbcnvgALT  5217  csbres  5307  csbrn  5500  sbcfung  5813  csbfv12  6126  csbfv2g  6127  elfvmptrab  6199  csbov  6564  csbov12g  6565  csbov1g  6566  csbov2g  6567  csbwrdg  13138  gsummptif1n0  18137  coe1fzgsumdlem  19441  evl1gsumdlem  19490  rusgrasn  26266  disjpreima  28573  esum2dlem  29275  csbwrecsg  32143  csbrecsg  32144  csbrdgg  32145  csbmpt22g  32147  f1omptsnlem  32153  relowlpssretop  32182  rdgeqoa  32188  csbfinxpg  32195  csbconstgi  32886  cdlemkid3N  35033  cdlemkid4  35034  cdlemk42  35041  brtrclfv2  36832  cotrclrcl  36847  frege77  37048  sbcel2gOLD  37570  onfrALTlem5  37572  onfrALTlem4  37573  csbfv12gALTOLD  37868  csbresgOLD  37871  onfrALTlem5VD  37937  onfrALTlem4VD  37938  csbsngVD  37945  csbxpgVD  37946  csbresgVD  37947  csbrngVD  37948  csbfv12gALTVD  37951  disjinfi  38169  iccelpart  39766