Theorem csbconstg 3865

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3864 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2213. (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 3849	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2762	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3847	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3810	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3455	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2827	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2897	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2787	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3517	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {cab 2738  Vcvv 3450  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sbc 3739  df-csb 3847

This theorem is used by:  csbconstgi  3867  csb0  4367  sbcel1g  4373  sbceq1g  4374  sbcel2  4375  sbceq2g  4376  csbidm  4390  2nreu  4401  csbopg  4850  sbcbr  5159  sbcbr12g  5160  sbcbr1g  5161  sbcbr2g  5162  csbmpt12  5528  csbmpt2  5529  sbcrel  5753  csbcnvgALTOLD  5862  csbres  5969  csbrn  6193  sbcfung  6551  sbcfungOLD  6552  csbfv12  6918  csbfv2g  6919  elfvmptrab  7011  csbov  7453  csbov12g  7454  csbov1g  7455  csbov2g  7456  csbfrecsg  8280  csbwrecsg  8314  csbwrdg  14657  gsummptif1n0  20142  coe1fzgsumdlem  22583  evl1gsumdlem  22636  opsbc2ie  33006  disjpreima  33112  esum2dlem  34658  csbrecsg  38171  csbrdgg  38172  csbmpo123  38174  f1omptsnlem  38179  relowlpssretop  38207  rdgeqoa  38213  csbfinxpg  38231  cdlemkid3N  41910  cdlemkid4  41911  cdlemk42  41918  minregex  44478  brtrclfv2  44671  cotrclrcl  44686  frege77  44884  onfrALTlem5  45469  onfrALTlem4  45470  onfrALTlem5VD  45811  onfrALTlem4VD  45812  csbsngVD  45819  csbxpgVD  45820  csbresgVD  45821  csbrngVD  45822  csbfv12gALTVD  45825  disjinfi  46128  eubrdm  48028  iccelpart  48437