Theorem csbconstg 3869

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3868 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2185. (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 3853	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2739	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3851	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3814	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3446	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2804	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2874	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2764	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3512	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3441  [wsbc 3741  ⦋csb 3850

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-sbc 3742  df-csb 3851

This theorem is referenced by:  csbconstgi  3871  csb0  4363  sbcel1g  4369  sbceq1g  4370  sbcel2  4371  sbceq2g  4372  csbidm  4386  2nreu  4397  csbopg  4848  sbcbr  5154  sbcbr12g  5155  sbcbr1g  5156  sbcbr2g  5157  csbmpt12  5506  csbmpt2  5507  sbcrel  5731  csbcnvgALT  5834  csbres  5942  csbrn  6162  sbcfung  6517  csbfv12  6880  csbfv2g  6881  elfvmptrab  6972  csbov  7405  csbov12g  7406  csbov1g  7407  csbov2g  7408  csbfrecsg  8228  csbwrecsg  8262  csbwrdg  14471  gsummptif1n0  19899  coe1fzgsumdlem  22251  evl1gsumdlem  22304  opsbc2ie  32532  disjpreima  32641  esum2dlem  34230  csbrecsg  37504  csbrdgg  37505  csbmpo123  37507  f1omptsnlem  37512  relowlpssretop  37540  rdgeqoa  37546  csbfinxpg  37564  cdlemkid3N  41230  cdlemkid4  41231  cdlemk42  41238  minregex  43811  brtrclfv2  44004  cotrclrcl  44019  frege77  44217  onfrALTlem5  44819  onfrALTlem4  44820  onfrALTlem5VD  45161  onfrALTlem4VD  45162  csbsngVD  45169  csbxpgVD  45170  csbresgVD  45171  csbrngVD  45172  csbfv12gALTVD  45175  disjinfi  45472  eubrdm  47318  iccelpart  47715