Theorem csbconstg 3940

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3939 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 3924	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2742	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3922	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3883	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3493	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2812	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2882	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2772	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3566	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  {cab 2717  Vcvv 3488  [wsbc 3804  ⦋csb 3921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-sbc 3805  df-csb 3922

This theorem is referenced by:  csbconstgi  3943  csb0  4433  sbcel1g  4439  sbceq1g  4440  sbcel2  4441  sbceq2g  4442  csbidm  4456  2nreu  4467  csbopg  4915  sbcbr  5221  sbcbr12g  5222  sbcbr1g  5223  sbcbr2g  5224  csbmpt12  5576  csbmpt2  5577  sbcrel  5804  csbcnvgALT  5909  csbres  6012  csbrn  6234  sbcfung  6602  csbfv12  6968  csbfv2g  6969  elfvmptrab  7058  csbov  7493  csbov12g  7494  csbov1g  7495  csbov2g  7496  csbfrecsg  8325  csbwrecsg  8362  csbwrdg  14592  gsummptif1n0  20008  coe1fzgsumdlem  22328  evl1gsumdlem  22381  opsbc2ie  32504  disjpreima  32606  esum2dlem  34056  csbrecsg  37294  csbrdgg  37295  csbmpo123  37297  f1omptsnlem  37302  relowlpssretop  37330  rdgeqoa  37336  csbfinxpg  37354  cdlemkid3N  40890  cdlemkid4  40891  cdlemk42  40898  minregex  43496  brtrclfv2  43689  cotrclrcl  43704  frege77  43902  onfrALTlem5  44513  onfrALTlem4  44514  onfrALTlem5VD  44856  onfrALTlem4VD  44857  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbfv12gALTVD  44870  disjinfi  45099  eubrdm  46951  iccelpart  47307