Theorem csbconstg 3917

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3916 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2176. (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 3901	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2738	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3899	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3862	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3484	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2808	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2878	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2768	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3553	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  {cab 2713  Vcvv 3479  [wsbc 3787  ⦋csb 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-sbc 3788  df-csb 3899

This theorem is referenced by:  csbconstgi  3919  csb0  4409  sbcel1g  4415  sbceq1g  4416  sbcel2  4417  sbceq2g  4418  csbidm  4432  2nreu  4443  csbopg  4890  sbcbr  5197  sbcbr12g  5198  sbcbr1g  5199  sbcbr2g  5200  csbmpt12  5561  csbmpt2  5562  sbcrel  5789  csbcnvgALT  5894  csbres  5999  csbrn  6222  sbcfung  6589  csbfv12  6953  csbfv2g  6954  elfvmptrab  7044  csbov  7477  csbov12g  7478  csbov1g  7479  csbov2g  7480  csbfrecsg  8310  csbwrecsg  8347  csbwrdg  14583  gsummptif1n0  19985  coe1fzgsumdlem  22308  evl1gsumdlem  22361  opsbc2ie  32496  disjpreima  32598  esum2dlem  34094  csbrecsg  37330  csbrdgg  37331  csbmpo123  37333  f1omptsnlem  37338  relowlpssretop  37366  rdgeqoa  37372  csbfinxpg  37390  cdlemkid3N  40936  cdlemkid4  40937  cdlemk42  40944  minregex  43552  brtrclfv2  43745  cotrclrcl  43760  frege77  43958  onfrALTlem5  44567  onfrALTlem4  44568  onfrALTlem5VD  44910  onfrALTlem4VD  44911  csbsngVD  44918  csbxpgVD  44919  csbresgVD  44920  csbrngVD  44921  csbfv12gALTVD  44924  disjinfi  45202  eubrdm  47053  iccelpart  47425