Theorem csbconstg 3881

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3880 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2178. (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 3865	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2731	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3863	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3826	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3452	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2796	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2865	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2756	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3520	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  Vcvv 3447  [wsbc 3753  ⦋csb 3862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-sbc 3754  df-csb 3863

This theorem is referenced by:  csbconstgi  3883  csb0  4373  sbcel1g  4379  sbceq1g  4380  sbcel2  4381  sbceq2g  4382  csbidm  4396  2nreu  4407  csbopg  4855  sbcbr  5162  sbcbr12g  5163  sbcbr1g  5164  sbcbr2g  5165  csbmpt12  5517  csbmpt2  5518  sbcrel  5743  csbcnvgALT  5848  csbres  5953  csbrn  6176  sbcfung  6540  csbfv12  6906  csbfv2g  6907  elfvmptrab  6997  csbov  7432  csbov12g  7433  csbov1g  7434  csbov2g  7435  csbfrecsg  8263  csbwrecsg  8297  csbwrdg  14509  gsummptif1n0  19896  coe1fzgsumdlem  22190  evl1gsumdlem  22243  opsbc2ie  32405  disjpreima  32513  esum2dlem  34082  csbrecsg  37316  csbrdgg  37317  csbmpo123  37319  f1omptsnlem  37324  relowlpssretop  37352  rdgeqoa  37358  csbfinxpg  37376  cdlemkid3N  40927  cdlemkid4  40928  cdlemk42  40935  minregex  43523  brtrclfv2  43716  cotrclrcl  43731  frege77  43929  onfrALTlem5  44532  onfrALTlem4  44533  onfrALTlem5VD  44874  onfrALTlem4VD  44875  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbfv12gALTVD  44888  disjinfi  45186  eubrdm  47037  iccelpart  47434