Theorem csbconstg 3855

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3854 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2174. (Revised by Gino Giotto, 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 3839	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2741	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3837	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3799	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3436	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2809	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2883	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2771	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3503	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2109  {cab 2716  Vcvv 3430  [wsbc 3719  ⦋csb 3836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-sbc 3720  df-csb 3837

This theorem is referenced by:  csbconstgi  3858  csb0  4346  sbcel1g  4352  sbceq1g  4353  sbcel2  4354  sbceq2g  4355  csbidm  4369  2nreu  4380  csbopg  4827  sbcbr  5133  sbcbr12g  5134  sbcbr1g  5135  sbcbr2g  5136  csbmpt12  5471  csbmpt2  5472  sbcrel  5689  csbcnvgALT  5790  csbres  5891  csbrn  6103  sbcfung  6454  csbfv12  6811  csbfv2g  6812  elfvmptrab  6897  csbov  7311  csbov12g  7312  csbov1g  7313  csbov2g  7314  csbfrecsg  8084  csbwrecsg  8121  csbwrdg  14228  gsummptif1n0  19548  coe1fzgsumdlem  21453  evl1gsumdlem  21503  opsbc2ie  30803  disjpreima  30902  esum2dlem  32039  csbrecsg  35478  csbrdgg  35479  csbmpo123  35481  f1omptsnlem  35486  relowlpssretop  35514  rdgeqoa  35520  csbfinxpg  35538  cdlemkid3N  38926  cdlemkid4  38927  cdlemk42  38934  brtrclfv2  41288  cotrclrcl  41303  frege77  41501  onfrALTlem5  42115  onfrALTlem4  42116  onfrALTlem5VD  42458  onfrALTlem4VD  42459  csbsngVD  42466  csbxpgVD  42467  csbresgVD  42468  csbrngVD  42469  csbfv12gALTVD  42472  disjinfi  42684  eubrdm  44481  iccelpart  44837