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