Theorem csbie 3873

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.)

Hypotheses

Ref	Expression
csbie.1	⊢ 𝐴 ∈ V
csbie.2	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
csbie	⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem csbie

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-csb 3839	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbie.1	. . . 4 ⊢ 𝐴 ∈ V
3		csbie.2	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	3	eleq2d 2826	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
5	2, 4	sbcie 3771	. . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)
6	5	abbii 2807	. 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶}
7		abid2 2877	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶
8	1, 6, 7	3eqtri 2767	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = 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-sbc 3731  df-csb 3839

This theorem is referenced by:  pofun  5551  eqerlem  8676  mptnn0fsuppd  13958  fsum  15680  fsumcnv  15733  fsumshftm  15741  fsum0diag2  15743  fprod  15904  fprodcnv  15946  bpolyval  16012  ruclem1  16196  odfval  19505  odval  19507  psrass1lem  21915  selvval  22103  mamufval  22382  pm2mpval  22785  isibl  25757  dfitg  25761  dvfsumlem2  26019  fsumdvdsmul  27183  precsexlem3  28226  disjxpin  32684  gsummulsubdishift2s  33159  poimirlem1  37989  poimirlem5  37993  poimirlem15  38003  poimirlem16  38004  poimirlem17  38005  poimirlem19  38007  poimirlem20  38008  poimirlem22  38010  poimirlem24  38012  poimirlem28  38016  evlselv  43040  fphpd  43262  monotuz  43387  oddcomabszz  43390  fnwe2val  43495  fnwe2lem1  43496  dfswapf2  49752  dfinito4  49992