Theorem csbie 3886

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 3852	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbie.1	. . . 4 ⊢ 𝐴 ∈ V
3		csbie.2	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	3	eleq2d 2823	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
5	2, 4	sbcie 3784	. . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)
6	5	abbii 2804	. 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶}
7		abid2 2874	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶
8	1, 6, 7	3eqtri 2764	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3442  [wsbc 3742  ⦋csb 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3743  df-csb 3852

This theorem is referenced by:  pofun  5558  eqerlem  8681  mptnn0fsuppd  13933  fsum  15655  fsumcnv  15708  fsumshftm  15716  fsum0diag2  15718  fprod  15876  fprodcnv  15918  bpolyval  15984  ruclem1  16168  odfval  19473  odval  19475  psrass1lem  21900  selvval  22090  mamufval  22348  pm2mpval  22751  isibl  25734  dfitg  25738  dvfsumlem2  26001  dvfsumlem2OLD  26002  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  precsexlem3  28217  disjxpin  32674  gsummulsubdishift2s  33164  poimirlem1  37861  poimirlem5  37865  poimirlem15  37875  poimirlem16  37876  poimirlem17  37877  poimirlem19  37879  poimirlem20  37880  poimirlem22  37882  poimirlem24  37884  poimirlem28  37888  evlselv  42934  fphpd  43162  monotuz  43287  oddcomabszz  43290  fnwe2val  43395  fnwe2lem1  43396  dfswapf2  49609  dfinito4  49849