Theorem csbconstg 3911

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3910 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2169. (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 3895	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2732	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3893	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3855	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3478	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2800	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2869	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2762	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3541	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  {cab 2707  Vcvv 3472  [wsbc 3776  ⦋csb 3892

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-sbc 3777  df-csb 3893

This theorem is referenced by:  csbconstgi  3914  csb0  4406  sbcel1g  4412  sbceq1g  4413  sbcel2  4414  sbceq2g  4415  csbidm  4429  2nreu  4440  csbopg  4890  sbcbr  5202  sbcbr12g  5203  sbcbr1g  5204  sbcbr2g  5205  csbmpt12  5556  csbmpt2  5557  sbcrel  5779  csbcnvgALT  5883  csbres  5983  csbrn  6201  sbcfung  6571  csbfv12  6938  csbfv2g  6939  elfvmptrab  7025  csbov  7454  csbov12g  7455  csbov1g  7456  csbov2g  7457  csbfrecsg  8271  csbwrecsg  8308  csbwrdg  14498  gsummptif1n0  19875  coe1fzgsumdlem  22045  evl1gsumdlem  22095  opsbc2ie  31983  disjpreima  32082  esum2dlem  33388  csbrecsg  36512  csbrdgg  36513  csbmpo123  36515  f1omptsnlem  36520  relowlpssretop  36548  rdgeqoa  36554  csbfinxpg  36572  cdlemkid3N  40107  cdlemkid4  40108  cdlemk42  40115  minregex  42587  brtrclfv2  42780  cotrclrcl  42795  frege77  42993  onfrALTlem5  43605  onfrALTlem4  43606  onfrALTlem5VD  43948  onfrALTlem4VD  43949  csbsngVD  43956  csbxpgVD  43957  csbresgVD  43958  csbrngVD  43959  csbfv12gALTVD  43962  disjinfi  44189  eubrdm  46044  iccelpart  46399