Theorem csbconstg 3870

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3869 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2216. (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 3854	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2765	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3852	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3814	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3459	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2830	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2901	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2790	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3521	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {cab 2741  Vcvv 3454  [wsbc 3742  ⦋csb 3851

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-sbc 3743  df-csb 3852

This theorem is used by:  csbconstgi  3872  csb0  4371  sbcel1g  4377  sbceq1g  4378  sbcel2  4379  sbceq2g  4380  csbidm  4394  2nreu  4405  csbopg  4854  sbcbr  5164  sbcbr12g  5165  sbcbr1g  5166  sbcbr2g  5167  csbmpt12  5536  csbmpt2  5537  sbcrel  5762  csbcnvgALTOLD  5873  csbres  5984  csbrn  6217  sbcfung  6583  sbcfungOLD  6584  csbfv12  6953  csbfv2g  6954  elfvmptrab  7046  csbov  7488  csbov12g  7489  csbov1g  7490  csbov2g  7491  csbfrecsg  8330  csbwrecsg  8364  csbwrdg  14716  gsummptif1n0  20210  coe1fzgsumdlem  22651  evl1gsumdlem  22704  opsbc2ie  33144  disjpreima  33250  esum2dlem  34794  csbrecsg  38443  csbrdgg  38444  csbmpo123  38446  f1omptsnlem  38451  relowlpssretop  38479  rdgeqoa  38485  csbfinxpg  38503  cdlemkid3N  42182  cdlemkid4  42183  cdlemk42  42190  minregex  44727  brtrclfv2  44919  cotrclrcl  44934  frege77  45132  onfrALTlem5  45716  onfrALTlem4  45717  onfrALTlem5VD  46058  onfrALTlem4VD  46059  csbsngVD  46066  csbxpgVD  46067  csbresgVD  46068  csbrngVD  46069  csbfv12gALTVD  46072  disjinfi  46412  eubrdm  48311  iccelpart  48720