Theorem csbconstg 3898

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3897 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2178. (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 3882	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2738	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3880	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3843	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3469	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2803	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2873	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2763	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3538	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2714  Vcvv 3464  [wsbc 3770  ⦋csb 3879

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-sbc 3771  df-csb 3880

This theorem is referenced by:  csbconstgi  3900  csb0  4390  sbcel1g  4396  sbceq1g  4397  sbcel2  4398  sbceq2g  4399  csbidm  4413  2nreu  4424  csbopg  4872  sbcbr  5179  sbcbr12g  5180  sbcbr1g  5181  sbcbr2g  5182  csbmpt12  5537  csbmpt2  5538  sbcrel  5764  csbcnvgALT  5869  csbres  5974  csbrn  6197  sbcfung  6565  csbfv12  6929  csbfv2g  6930  elfvmptrab  7020  csbov  7455  csbov12g  7456  csbov1g  7457  csbov2g  7458  csbfrecsg  8288  csbwrecsg  8325  csbwrdg  14567  gsummptif1n0  19952  coe1fzgsumdlem  22246  evl1gsumdlem  22299  opsbc2ie  32462  disjpreima  32570  esum2dlem  34128  csbrecsg  37351  csbrdgg  37352  csbmpo123  37354  f1omptsnlem  37359  relowlpssretop  37387  rdgeqoa  37393  csbfinxpg  37411  cdlemkid3N  40957  cdlemkid4  40958  cdlemk42  40965  minregex  43533  brtrclfv2  43726  cotrclrcl  43741  frege77  43939  onfrALTlem5  44542  onfrALTlem4  44543  onfrALTlem5VD  44884  onfrALTlem4VD  44885  csbsngVD  44892  csbxpgVD  44893  csbresgVD  44894  csbrngVD  44895  csbfv12gALTVD  44898  disjinfi  45196  eubrdm  47045  iccelpart  47427