Theorem csbconstg 3857

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3856 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2185. (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 3841	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2739	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3839	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3802	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3435	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2804	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2874	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2764	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3500	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3430  [wsbc 3729  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbconstgi  3859  csb0  4351  sbcel1g  4357  sbceq1g  4358  sbcel2  4359  sbceq2g  4360  csbidm  4374  2nreu  4385  csbopg  4835  sbcbr  5141  sbcbr12g  5142  sbcbr1g  5143  sbcbr2g  5144  csbmpt12  5503  csbmpt2  5504  sbcrel  5728  csbcnvgALT  5831  csbres  5939  csbrn  6159  sbcfung  6514  csbfv12  6877  csbfv2g  6878  elfvmptrab  6969  csbov  7403  csbov12g  7404  csbov1g  7405  csbov2g  7406  csbfrecsg  8225  csbwrecsg  8259  csbwrdg  14495  gsummptif1n0  19930  coe1fzgsumdlem  22277  evl1gsumdlem  22330  opsbc2ie  32565  disjpreima  32674  esum2dlem  34257  csbrecsg  37655  csbrdgg  37656  csbmpo123  37658  f1omptsnlem  37663  relowlpssretop  37691  rdgeqoa  37697  csbfinxpg  37715  cdlemkid3N  41390  cdlemkid4  41391  cdlemk42  41398  minregex  43976  brtrclfv2  44169  cotrclrcl  44184  frege77  44382  onfrALTlem5  44984  onfrALTlem4  44985  onfrALTlem5VD  45326  onfrALTlem4VD  45327  csbsngVD  45334  csbxpgVD  45335  csbresgVD  45336  csbrngVD  45337  csbfv12gALTVD  45340  disjinfi  45637  eubrdm  47481  iccelpart  47890