Theorem csbconstg 3909

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3908 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2166. (Revised by Gino Giotto, 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 3893	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2727	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3891	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3853	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3469	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2795	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2863	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2757	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3533	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {cab 2702  Vcvv 3463  [wsbc 3774  ⦋csb 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465  df-sbc 3775  df-csb 3891

This theorem is referenced by:  csbconstgi  3912  csb0  4408  sbcel1g  4414  sbceq1g  4415  sbcel2  4416  sbceq2g  4417  csbidm  4431  2nreu  4442  csbopg  4892  sbcbr  5203  sbcbr12g  5204  sbcbr1g  5205  sbcbr2g  5206  csbmpt12  5558  csbmpt2  5559  sbcrel  5781  csbcnvgALT  5886  csbres  5987  csbrn  6207  sbcfung  6576  csbfv12  6942  csbfv2g  6943  elfvmptrab  7031  csbov  7461  csbov12g  7462  csbov1g  7463  csbov2g  7464  csbfrecsg  8288  csbwrecsg  8325  csbwrdg  14526  gsummptif1n0  19925  coe1fzgsumdlem  22231  evl1gsumdlem  22284  opsbc2ie  32331  disjpreima  32431  esum2dlem  33781  csbrecsg  36877  csbrdgg  36878  csbmpo123  36880  f1omptsnlem  36885  relowlpssretop  36913  rdgeqoa  36919  csbfinxpg  36937  cdlemkid3N  40475  cdlemkid4  40476  cdlemk42  40483  minregex  43029  brtrclfv2  43222  cotrclrcl  43237  frege77  43435  onfrALTlem5  44046  onfrALTlem4  44047  onfrALTlem5VD  44389  onfrALTlem4VD  44390  csbsngVD  44397  csbxpgVD  44398  csbresgVD  44399  csbrngVD  44400  csbfv12gALTVD  44403  disjinfi  44629  eubrdm  46481  iccelpart  46836