Theorem csbconstg 3884

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3883 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 3868	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2732	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3866	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3829	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3455	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2797	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2866	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2757	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3523	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2708  Vcvv 3450  [wsbc 3756  ⦋csb 3865

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-sbc 3757  df-csb 3866

This theorem is referenced by:  csbconstgi  3886  csb0  4376  sbcel1g  4382  sbceq1g  4383  sbcel2  4384  sbceq2g  4385  csbidm  4399  2nreu  4410  csbopg  4858  sbcbr  5165  sbcbr12g  5166  sbcbr1g  5167  sbcbr2g  5168  csbmpt12  5520  csbmpt2  5521  sbcrel  5746  csbcnvgALT  5851  csbres  5956  csbrn  6179  sbcfung  6543  csbfv12  6909  csbfv2g  6910  elfvmptrab  7000  csbov  7435  csbov12g  7436  csbov1g  7437  csbov2g  7438  csbfrecsg  8266  csbwrecsg  8300  csbwrdg  14516  gsummptif1n0  19903  coe1fzgsumdlem  22197  evl1gsumdlem  22250  opsbc2ie  32412  disjpreima  32520  esum2dlem  34089  csbrecsg  37323  csbrdgg  37324  csbmpo123  37326  f1omptsnlem  37331  relowlpssretop  37359  rdgeqoa  37365  csbfinxpg  37383  cdlemkid3N  40934  cdlemkid4  40935  cdlemk42  40942  minregex  43530  brtrclfv2  43723  cotrclrcl  43738  frege77  43936  onfrALTlem5  44539  onfrALTlem4  44540  onfrALTlem5VD  44881  onfrALTlem4VD  44882  csbsngVD  44889  csbxpgVD  44890  csbresgVD  44891  csbrngVD  44892  csbfv12gALTVD  44895  disjinfi  45193  eubrdm  47041  iccelpart  47438