Theorem csbconstg 3871

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142  {cab 2740  Vcvv 3454  [wsbc 3743  ⦋csb 3852

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-sbc 3744  df-csb 3853

This theorem is used by:  csbconstgi  3873  csb0  4374  sbcel1g  4380  sbceq1g  4381  sbcel2  4382  sbceq2g  4383  csbidm  4397  2nreu  4408  csbopg  4855  sbcbr  5165  sbcbr12g  5166  sbcbr1g  5167  sbcbr2g  5168  csbmpt12  5541  csbmpt2  5542  sbcrel  5766  csbcnvgALTOLD  5873  csbres  5980  csbrn  6203  sbcfung  6560  csbfv12  6926  csbfv2g  6927  elfvmptrab  7019  csbov  7457  csbov12g  7458  csbov1g  7459  csbov2g  7460  csbfrecsg  8279  csbwrecsg  8313  csbwrdg  14588  gsummptif1n0  20042  coe1fzgsumdlem  22474  evl1gsumdlem  22527  opsbc2ie  32833  disjpreima  32940  esum2dlem  34491  csbrecsg  38002  csbrdgg  38003  csbmpo123  38005  f1omptsnlem  38010  relowlpssretop  38038  rdgeqoa  38044  csbfinxpg  38062  cdlemkid3N  41735  cdlemkid4  41736  cdlemk42  41743  minregex  44288  brtrclfv2  44481  cotrclrcl  44496  frege77  44694  onfrALTlem5  45279  onfrALTlem4  45280  onfrALTlem5VD  45621  onfrALTlem4VD  45622  csbsngVD  45629  csbxpgVD  45630  csbresgVD  45631  csbrngVD  45632  csbfv12gALTVD  45635  disjinfi  45938  eubrdm  47801  iccelpart  48210