Theorem csbconstg 3579

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

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030  ⦋csb 3566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sbc 3469  df-csb 3567

This theorem is referenced by:  csb0  4015  sbcel1g  4020  sbceq1g  4021  sbcel2  4022  sbceq2g  4023  csbidm  4035  csbopg  4451  sbcbr  4740  sbcbr12g  4741  sbcbr1g  4742  sbcbr2g  4743  csbmpt12  5039  csbmpt2  5040  sbcrel  5239  csbcnvgALT  5339  csbres  5431  csbrn  5631  sbcfung  5950  csbfv12  6269  csbfv2g  6270  elfvmptrab  6345  csbov  6728  csbov12g  6729  csbov1g  6730  csbov2g  6731  csbwrdg  13366  gsummptif1n0  18411  coe1fzgsumdlem  19719  evl1gsumdlem  19768  disjpreima  29523  esum2dlem  30282  csbwrecsg  33303  csbrecsg  33304  csbrdgg  33305  csbmpt22g  33307  f1omptsnlem  33313  relowlpssretop  33342  rdgeqoa  33348  csbfinxpg  33355  csbconstgi  34052  cdlemkid3N  36538  cdlemkid4  36539  cdlemk42  36546  brtrclfv2  38336  cotrclrcl  38351  frege77  38551  sbcel2gOLD  39072  onfrALTlem5  39074  onfrALTlem4  39075  csbresgOLD  39370  onfrALTlem5VD  39435  onfrALTlem4VD  39436  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbfv12gALTVD  39449  disjinfi  39694  iccelpart  41694