Theorem csbconstg 3874

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3873 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2215. (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 3858	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2767	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3856	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3819	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3462	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2832	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2902	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2792	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3525	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  {cab 2743  Vcvv 3457  [wsbc 3747  ⦋csb 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-sbc 3748  df-csb 3856

This theorem is referenced by:  csbconstgi  3876  csb0  4367  sbcel1g  4373  sbceq1g  4374  sbcel2  4375  sbceq2g  4376  csbidm  4390  2nreu  4401  csbopg  4852  sbcbr  5160  sbcbr12g  5161  sbcbr1g  5162  sbcbr2g  5163  csbmpt12  5533  csbmpt2  5534  sbcrel  5758  csbcnvgALTOLD  5865  csbres  5972  csbrn  6194  sbcfung  6549  csbfv12  6916  csbfv2g  6917  elfvmptrab  7009  csbov  7445  csbov12g  7446  csbov1g  7447  csbov2g  7448  csbfrecsg  8269  csbwrecsg  8303  csbwrdg  14571  gsummptif1n0  20027  coe1fzgsumdlem  22424  evl1gsumdlem  22477  opsbc2ie  32732  disjpreima  32839  esum2dlem  34399  csbrecsg  37834  csbrdgg  37835  csbmpo123  37837  f1omptsnlem  37842  relowlpssretop  37870  rdgeqoa  37876  csbfinxpg  37894  cdlemkid3N  41569  cdlemkid4  41570  cdlemk42  41577  minregex  44122  brtrclfv2  44315  cotrclrcl  44330  frege77  44528  onfrALTlem5  45116  onfrALTlem4  45117  onfrALTlem5VD  45458  onfrALTlem4VD  45459  csbsngVD  45466  csbxpgVD  45467  csbresgVD  45468  csbrngVD  45469  csbfv12gALTVD  45472  disjinfi  45768  eubrdm  47628  iccelpart  48037