Theorem csbconstg 3546

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  ⦋csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sbc 3436  df-csb 3534

This theorem is referenced by:  csb0  3982  sbcel1g  3987  sbceq1g  3988  sbcel2  3989  sbceq2g  3990  csbidm  4002  csbopg  4420  sbcbr  4707  sbcbr12g  4708  sbcbr1g  4709  sbcbr2g  4710  csbmpt12  5010  csbmpt2  5011  sbcrel  5205  csbcnvgALT  5307  csbres  5399  csbrn  5596  sbcfung  5912  csbfv12  6231  csbfv2g  6232  elfvmptrab  6306  csbov  6688  csbov12g  6689  csbov1g  6690  csbov2g  6691  csbwrdg  13334  gsummptif1n0  18365  coe1fzgsumdlem  19671  evl1gsumdlem  19720  disjpreima  29397  esum2dlem  30154  csbwrecsg  33173  csbrecsg  33174  csbrdgg  33175  csbmpt22g  33177  f1omptsnlem  33183  relowlpssretop  33212  rdgeqoa  33218  csbfinxpg  33225  csbconstgi  33922  cdlemkid3N  36221  cdlemkid4  36222  cdlemk42  36229  brtrclfv2  38019  cotrclrcl  38034  frege77  38234  sbcel2gOLD  38755  onfrALTlem5  38757  onfrALTlem4  38758  csbfv12gALTOLD  39052  csbresgOLD  39055  onfrALTlem5VD  39121  onfrALTlem4VD  39122  csbsngVD  39129  csbxpgVD  39130  csbresgVD  39131  csbrngVD  39132  csbfv12gALTVD  39135  disjinfi  39380  iccelpart  41369