Theorem csbconstg 3865

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3864 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2212. (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 3849	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2762	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3847	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3810	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3455	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2827	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2897	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2787	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3517	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {cab 2738  Vcvv 3450  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sbc 3739  df-csb 3847

This theorem is used by:  csbconstgi  3867  csb0  4367  sbcel1g  4373  sbceq1g  4374  sbcel2  4375  sbceq2g  4376  csbidm  4390  2nreu  4401  csbopg  4850  sbcbr  5160  sbcbr12g  5161  sbcbr1g  5162  sbcbr2g  5163  csbmpt12  5531  csbmpt2  5532  sbcrel  5756  csbcnvgALTOLD  5865  csbres  5972  csbrn  6204  sbcfung  6563  sbcfungOLD  6564  csbfv12  6930  csbfv2g  6931  elfvmptrab  7023  csbov  7465  csbov12g  7466  csbov1g  7467  csbov2g  7468  csbfrecsg  8303  csbwrecsg  8337  csbwrdg  14690  gsummptif1n0  20181  coe1fzgsumdlem  22622  evl1gsumdlem  22675  opsbc2ie  33115  disjpreima  33221  esum2dlem  34767  csbrecsg  38327  csbrdgg  38328  csbmpo123  38330  f1omptsnlem  38335  relowlpssretop  38363  rdgeqoa  38369  csbfinxpg  38387  cdlemkid3N  42066  cdlemkid4  42067  cdlemk42  42074  minregex  44611  brtrclfv2  44803  cotrclrcl  44818  frege77  45016  onfrALTlem5  45601  onfrALTlem4  45602  onfrALTlem5VD  45943  onfrALTlem4VD  45944  csbsngVD  45951  csbxpgVD  45952  csbresgVD  45953  csbrngVD  45954  csbfv12gALTVD  45957  disjinfi  46283  eubrdm  48182  iccelpart  48591