Theorem csbconstg 3866

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3865 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2206. (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 3850	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2758	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3848	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3811	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3453	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2823	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2893	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2783	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3516	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1554   ∈ wcel 2136  {cab 2734  Vcvv 3448  [wsbc 3739  ⦋csb 3847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-v 3450  df-sbc 3740  df-csb 3848

This theorem is referenced by:  csbconstgi  3868  csb0  4358  sbcel1g  4364  sbceq1g  4365  sbcel2  4366  sbceq2g  4367  csbidm  4381  2nreu  4392  csbopg  4843  sbcbr  5149  sbcbr12g  5150  sbcbr1g  5151  sbcbr2g  5152  csbmpt12  5521  csbmpt2  5522  sbcrel  5746  csbcnvgALTOLD  5853  csbres  5961  csbrn  6179  sbcfung  6534  csbfv12  6901  csbfv2g  6902  elfvmptrab  6994  csbov  7430  csbov12g  7431  csbov1g  7432  csbov2g  7433  csbfrecsg  8253  csbwrecsg  8287  csbwrdg  14547  gsummptif1n0  19982  coe1fzgsumdlem  22339  evl1gsumdlem  22392  opsbc2ie  32616  disjpreima  32726  esum2dlem  34343  csbrecsg  37770  csbrdgg  37771  csbmpo123  37773  f1omptsnlem  37778  relowlpssretop  37806  rdgeqoa  37812  csbfinxpg  37830  cdlemkid3N  41505  cdlemkid4  41506  cdlemk42  41513  minregex  44058  brtrclfv2  44251  cotrclrcl  44266  frege77  44464  onfrALTlem5  45066  onfrALTlem4  45067  onfrALTlem5VD  45408  onfrALTlem4VD  45409  csbsngVD  45416  csbxpgVD  45417  csbresgVD  45418  csbrngVD  45419  csbfv12gALTVD  45422  disjinfi  45718  eubrdm  47578  iccelpart  47987