Theorem csbconstg 3905

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3904 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2171. (Revised by Gino Giotto, 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 3889	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2733	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3887	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3849	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3476	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2801	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2870	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2763	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3550	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {cab 2708  Vcvv 3470  [wsbc 3770  ⦋csb 3886

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3472  df-sbc 3771  df-csb 3887

This theorem is referenced by:  csbconstgi  3908  csb0  4400  sbcel1g  4406  sbceq1g  4407  sbcel2  4408  sbceq2g  4409  csbidm  4423  2nreu  4434  csbopg  4881  sbcbr  5193  sbcbr12g  5194  sbcbr1g  5195  sbcbr2g  5196  csbmpt12  5547  csbmpt2  5548  sbcrel  5769  csbcnvgALT  5873  csbres  5973  csbrn  6188  sbcfung  6558  csbfv12  6923  csbfv2g  6924  elfvmptrab  7009  csbov  7433  csbov12g  7434  csbov1g  7435  csbov2g  7436  csbfrecsg  8248  csbwrecsg  8285  csbwrdg  14473  gsummptif1n0  19790  coe1fzgsumdlem  21749  evl1gsumdlem  21799  opsbc2ie  31574  disjpreima  31675  esum2dlem  32905  csbrecsg  35997  csbrdgg  35998  csbmpo123  36000  f1omptsnlem  36005  relowlpssretop  36033  rdgeqoa  36039  csbfinxpg  36057  cdlemkid3N  39593  cdlemkid4  39594  cdlemk42  39601  minregex  42042  brtrclfv2  42235  cotrclrcl  42250  frege77  42448  onfrALTlem5  43060  onfrALTlem4  43061  onfrALTlem5VD  43403  onfrALTlem4VD  43404  csbsngVD  43411  csbxpgVD  43412  csbresgVD  43413  csbrngVD  43414  csbfv12gALTVD  43417  disjinfi  43648  eubrdm  45504  iccelpart  45859