Theorem csbconstg 3867

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3866 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2179. (Revised by GG, 15-Oct-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐵

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

Proof of Theorem csbconstg

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbeq1 3851	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2732	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3849	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3812	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3439	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2797	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2866	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2757	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3507	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2110  {cab 2708  Vcvv 3434  [wsbc 3739  ⦋csb 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-sbc 3740  df-csb 3849

This theorem is referenced by:  csbconstgi  3869  csb0  4358  sbcel1g  4364  sbceq1g  4365  sbcel2  4366  sbceq2g  4367  csbidm  4381  2nreu  4392  csbopg  4841  sbcbr  5144  sbcbr12g  5145  sbcbr1g  5146  sbcbr2g  5147  csbmpt12  5495  csbmpt2  5496  sbcrel  5719  csbcnvgALT  5822  csbres  5928  csbrn  6147  sbcfung  6501  csbfv12  6862  csbfv2g  6863  elfvmptrab  6953  csbov  7386  csbov12g  7387  csbov1g  7388  csbov2g  7389  csbfrecsg  8209  csbwrecsg  8243  csbwrdg  14443  gsummptif1n0  19871  coe1fzgsumdlem  22211  evl1gsumdlem  22264  opsbc2ie  32445  disjpreima  32554  esum2dlem  34095  csbrecsg  37341  csbrdgg  37342  csbmpo123  37344  f1omptsnlem  37349  relowlpssretop  37377  rdgeqoa  37383  csbfinxpg  37401  cdlemkid3N  40951  cdlemkid4  40952  cdlemk42  40959  minregex  43546  brtrclfv2  43739  cotrclrcl  43754  frege77  43952  onfrALTlem5  44554  onfrALTlem4  44555  onfrALTlem5VD  44896  onfrALTlem4VD  44897  csbsngVD  44904  csbxpgVD  44905  csbresgVD  44906  csbrngVD  44907  csbfv12gALTVD  44910  disjinfi  45208  eubrdm  47046  iccelpart  47443