Theorem csbconstg 3870

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3869 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2185. (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 3854	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2739	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3852	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3815	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3447	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2804	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2874	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2764	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3513	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3442  [wsbc 3742  ⦋csb 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-sbc 3743  df-csb 3852

This theorem is referenced by:  csbconstgi  3872  csb0  4364  sbcel1g  4370  sbceq1g  4371  sbcel2  4372  sbceq2g  4373  csbidm  4387  2nreu  4398  csbopg  4849  sbcbr  5155  sbcbr12g  5156  sbcbr1g  5157  sbcbr2g  5158  csbmpt12  5513  csbmpt2  5514  sbcrel  5738  csbcnvgALT  5841  csbres  5949  csbrn  6169  sbcfung  6524  csbfv12  6887  csbfv2g  6888  elfvmptrab  6979  csbov  7413  csbov12g  7414  csbov1g  7415  csbov2g  7416  csbfrecsg  8236  csbwrecsg  8270  csbwrdg  14479  gsummptif1n0  19907  coe1fzgsumdlem  22259  evl1gsumdlem  22312  opsbc2ie  32561  disjpreima  32670  esum2dlem  34269  csbrecsg  37572  csbrdgg  37573  csbmpo123  37575  f1omptsnlem  37580  relowlpssretop  37608  rdgeqoa  37614  csbfinxpg  37632  cdlemkid3N  41298  cdlemkid4  41299  cdlemk42  41306  minregex  43879  brtrclfv2  44072  cotrclrcl  44087  frege77  44285  onfrALTlem5  44887  onfrALTlem4  44888  onfrALTlem5VD  45229  onfrALTlem4VD  45230  csbsngVD  45237  csbxpgVD  45238  csbresgVD  45239  csbrngVD  45240  csbfv12gALTVD  45243  disjinfi  45540  eubrdm  47385  iccelpart  47782