Theorem csbconstg 3872

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3871 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 3856	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2731	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3854	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3817	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3443	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2796	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2865	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2756	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3511	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  Vcvv 3438  [wsbc 3744  ⦋csb 3853

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 3440  df-sbc 3745  df-csb 3854

This theorem is referenced by:  csbconstgi  3874  csb0  4363  sbcel1g  4369  sbceq1g  4370  sbcel2  4371  sbceq2g  4372  csbidm  4386  2nreu  4397  csbopg  4845  sbcbr  5150  sbcbr12g  5151  sbcbr1g  5152  sbcbr2g  5153  csbmpt12  5504  csbmpt2  5505  sbcrel  5728  csbcnvgALT  5831  csbres  5937  csbrn  6156  sbcfung  6510  csbfv12  6872  csbfv2g  6873  elfvmptrab  6963  csbov  7398  csbov12g  7399  csbov1g  7400  csbov2g  7401  csbfrecsg  8224  csbwrecsg  8258  csbwrdg  14469  gsummptif1n0  19863  coe1fzgsumdlem  22206  evl1gsumdlem  22259  opsbc2ie  32438  disjpreima  32546  esum2dlem  34058  csbrecsg  37301  csbrdgg  37302  csbmpo123  37304  f1omptsnlem  37309  relowlpssretop  37337  rdgeqoa  37343  csbfinxpg  37361  cdlemkid3N  40912  cdlemkid4  40913  cdlemk42  40920  minregex  43507  brtrclfv2  43700  cotrclrcl  43715  frege77  43913  onfrALTlem5  44516  onfrALTlem4  44517  onfrALTlem5VD  44858  onfrALTlem4VD  44859  csbsngVD  44866  csbxpgVD  44867  csbresgVD  44868  csbrngVD  44869  csbfv12gALTVD  44872  disjinfi  45170  eubrdm  47021  iccelpart  47418