Theorem csbconstg 3868

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {cab 2714  Vcvv 3440  [wsbc 3740  ⦋csb 3849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-sbc 3741  df-csb 3850

This theorem is referenced by:  csbconstgi  3870  csb0  4362  sbcel1g  4368  sbceq1g  4369  sbcel2  4370  sbceq2g  4371  csbidm  4385  2nreu  4396  csbopg  4847  sbcbr  5153  sbcbr12g  5154  sbcbr1g  5155  sbcbr2g  5156  csbmpt12  5505  csbmpt2  5506  sbcrel  5730  csbcnvgALT  5833  csbres  5941  csbrn  6161  sbcfung  6516  csbfv12  6879  csbfv2g  6880  elfvmptrab  6970  csbov  7403  csbov12g  7404  csbov1g  7405  csbov2g  7406  csbfrecsg  8226  csbwrecsg  8260  csbwrdg  14467  gsummptif1n0  19895  coe1fzgsumdlem  22247  evl1gsumdlem  22300  opsbc2ie  32550  disjpreima  32659  esum2dlem  34249  csbrecsg  37529  csbrdgg  37530  csbmpo123  37532  f1omptsnlem  37537  relowlpssretop  37565  rdgeqoa  37571  csbfinxpg  37589  cdlemkid3N  41189  cdlemkid4  41190  cdlemk42  41197  minregex  43771  brtrclfv2  43964  cotrclrcl  43979  frege77  44177  onfrALTlem5  44779  onfrALTlem4  44780  onfrALTlem5VD  45121  onfrALTlem4VD  45122  csbsngVD  45129  csbxpgVD  45130  csbresgVD  45131  csbrngVD  45132  csbfv12gALTVD  45135  disjinfi  45432  eubrdm  47278  iccelpart  47675