Theorem csbconstg 3857

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3856 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 3841	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2739	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3839	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3802	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3435	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2804	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2874	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2764	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3500	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3430  [wsbc 3729  ⦋csb 3838

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 3432  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbconstgi  3859  csb0  4351  sbcel1g  4357  sbceq1g  4358  sbcel2  4359  sbceq2g  4360  csbidm  4374  2nreu  4385  csbopg  4835  sbcbr  5141  sbcbr12g  5142  sbcbr1g  5143  sbcbr2g  5144  csbmpt12  5512  csbmpt2  5513  sbcrel  5737  csbcnvgALT  5840  csbres  5948  csbrn  6168  sbcfung  6523  csbfv12  6886  csbfv2g  6887  elfvmptrab  6978  csbov  7412  csbov12g  7413  csbov1g  7414  csbov2g  7415  csbfrecsg  8234  csbwrecsg  8268  csbwrdg  14506  gsummptif1n0  19941  coe1fzgsumdlem  22268  evl1gsumdlem  22321  opsbc2ie  32545  disjpreima  32654  esum2dlem  34236  csbrecsg  37644  csbrdgg  37645  csbmpo123  37647  f1omptsnlem  37652  relowlpssretop  37680  rdgeqoa  37686  csbfinxpg  37704  cdlemkid3N  41379  cdlemkid4  41380  cdlemk42  41387  minregex  43961  brtrclfv2  44154  cotrclrcl  44169  frege77  44367  onfrALTlem5  44969  onfrALTlem4  44970  onfrALTlem5VD  45311  onfrALTlem4VD  45312  csbsngVD  45319  csbxpgVD  45320  csbresgVD  45321  csbrngVD  45322  csbfv12gALTVD  45325  disjinfi  45622  eubrdm  47478  iccelpart  47887