Theorem csbconstg 3927

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3926 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2175. (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 3911	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2737	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3909	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3870	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3483	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2807	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2877	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2767	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3554	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {cab 2712  Vcvv 3478  [wsbc 3791  ⦋csb 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-sbc 3792  df-csb 3909

This theorem is referenced by:  csbconstgi  3930  csb0  4416  sbcel1g  4422  sbceq1g  4423  sbcel2  4424  sbceq2g  4425  csbidm  4439  2nreu  4450  csbopg  4896  sbcbr  5203  sbcbr12g  5204  sbcbr1g  5205  sbcbr2g  5206  csbmpt12  5567  csbmpt2  5568  sbcrel  5793  csbcnvgALT  5898  csbres  6003  csbrn  6225  sbcfung  6592  csbfv12  6955  csbfv2g  6956  elfvmptrab  7045  csbov  7476  csbov12g  7477  csbov1g  7478  csbov2g  7479  csbfrecsg  8308  csbwrecsg  8345  csbwrdg  14579  gsummptif1n0  19999  coe1fzgsumdlem  22323  evl1gsumdlem  22376  opsbc2ie  32504  disjpreima  32604  esum2dlem  34073  csbrecsg  37311  csbrdgg  37312  csbmpo123  37314  f1omptsnlem  37319  relowlpssretop  37347  rdgeqoa  37353  csbfinxpg  37371  cdlemkid3N  40916  cdlemkid4  40917  cdlemk42  40924  minregex  43524  brtrclfv2  43717  cotrclrcl  43732  frege77  43930  onfrALTlem5  44540  onfrALTlem4  44541  onfrALTlem5VD  44883  onfrALTlem4VD  44884  csbsngVD  44891  csbxpgVD  44892  csbresgVD  44893  csbrngVD  44894  csbfv12gALTVD  44897  disjinfi  45135  eubrdm  46986  iccelpart  47358