Theorem csbconstg 3913

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3912 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2172. (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 3897	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2735	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3895	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3857	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3481	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2803	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2872	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2765	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3557	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {cab 2710  Vcvv 3475  [wsbc 3778  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbconstgi  3916  csb0  4408  sbcel1g  4414  sbceq1g  4415  sbcel2  4416  sbceq2g  4417  csbidm  4431  2nreu  4442  csbopg  4892  sbcbr  5204  sbcbr12g  5205  sbcbr1g  5206  sbcbr2g  5207  csbmpt12  5558  csbmpt2  5559  sbcrel  5781  csbcnvgALT  5885  csbres  5985  csbrn  6203  sbcfung  6573  csbfv12  6940  csbfv2g  6941  elfvmptrab  7027  csbov  7452  csbov12g  7453  csbov1g  7454  csbov2g  7455  csbfrecsg  8269  csbwrecsg  8306  csbwrdg  14494  gsummptif1n0  19834  coe1fzgsumdlem  21825  evl1gsumdlem  21875  opsbc2ie  31716  disjpreima  31815  esum2dlem  33090  csbrecsg  36209  csbrdgg  36210  csbmpo123  36212  f1omptsnlem  36217  relowlpssretop  36245  rdgeqoa  36251  csbfinxpg  36269  cdlemkid3N  39804  cdlemkid4  39805  cdlemk42  39812  minregex  42285  brtrclfv2  42478  cotrclrcl  42493  frege77  42691  onfrALTlem5  43303  onfrALTlem4  43304  onfrALTlem5VD  43646  onfrALTlem4VD  43647  csbsngVD  43654  csbxpgVD  43655  csbresgVD  43656  csbrngVD  43657  csbfv12gALTVD  43660  disjinfi  43891  eubrdm  45746  iccelpart  46101