Theorem csbconstg 3857

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {cab 2718  Vcvv 3432  [wsbc 3730  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-sbc 3731  df-csb 3839

This theorem is referenced by:  csbconstgi  3859  csb0  4345  sbcel1g  4351  sbceq1g  4352  sbcel2  4353  sbceq2g  4354  csbidm  4368  2nreu  4379  csbopg  4829  sbcbr  5134  sbcbr12g  5135  sbcbr1g  5136  sbcbr2g  5137  csbmpt12  5506  csbmpt2  5507  sbcrel  5731  csbcnvgALT  5833  csbres  5941  csbrn  6161  sbcfung  6516  csbfv12  6879  csbfv2g  6880  elfvmptrab  6972  csbov  7408  csbov12g  7409  csbov1g  7410  csbov2g  7411  csbfrecsg  8231  csbwrecsg  8265  csbwrdg  14504  gsummptif1n0  19939  coe1fzgsumdlem  22296  evl1gsumdlem  22349  opsbc2ie  32570  disjpreima  32680  esum2dlem  34283  csbrecsg  37691  csbrdgg  37692  csbmpo123  37694  f1omptsnlem  37699  relowlpssretop  37727  rdgeqoa  37733  csbfinxpg  37751  cdlemkid3N  41426  cdlemkid4  41427  cdlemk42  41434  minregex  43979  brtrclfv2  44172  cotrclrcl  44187  frege77  44385  onfrALTlem5  44987  onfrALTlem4  44988  onfrALTlem5VD  45329  onfrALTlem4VD  45330  csbsngVD  45337  csbxpgVD  45338  csbresgVD  45339  csbrngVD  45340  csbfv12gALTVD  45343  disjinfi  45640  eubrdm  47500  iccelpart  47909