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  8302  csbwrecsg  8336  csbwrdg  14689  gsummptif1n0  20180  coe1fzgsumdlem  22621  evl1gsumdlem  22674  opsbc2ie  33114  disjpreima  33220  esum2dlem  34766  csbrecsg  38294  csbrdgg  38295  csbmpo123  38297  f1omptsnlem  38302  relowlpssretop  38330  rdgeqoa  38336  csbfinxpg  38354  cdlemkid3N  42033  cdlemkid4  42034  cdlemk42  42041  minregex  44577  brtrclfv2  44769  cotrclrcl  44784  frege77  44982  onfrALTlem5  45567  onfrALTlem4  45568  onfrALTlem5VD  45909  onfrALTlem4VD  45910  csbsngVD  45917  csbxpgVD  45918  csbresgVD  45919  csbrngVD  45920  csbfv12gALTVD  45923  disjinfi  46249  eubrdm  48148  iccelpart  48557