Theorem csbie 3907

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 3873	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbie.1	. . . 4 ⊢ 𝐴 ∈ V
3		csbie.2	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	3	eleq2d 2819	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
5	2, 4	sbcie 3805	. . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)
6	5	abbii 2801	. 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶}
7		abid2 2871	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶
8	1, 6, 7	3eqtri 2761	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  {cab 2712  Vcvv 3457  [wsbc 3763  ⦋csb 3872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-sbc 3764  df-csb 3873

This theorem is referenced by:  pofun  5576  eqerlem  8748  mptnn0fsuppd  14005  fsum  15723  fsumcnv  15776  fsumshftm  15784  fsum0diag2  15786  fprod  15944  fprodcnv  15986  bpolyval  16052  ruclem1  16234  odfval  19498  odval  19500  psrass1lem  21877  selvval  22058  mamufval  22315  pm2mpval  22718  isibl  25703  dfitg  25707  dvfsumlem2  25970  dvfsumlem2OLD  25971  fsumdvdsmul  27141  fsumdvdsmulOLD  27143  precsexlem3  28136  disjxpin  32502  poimirlem1  37566  poimirlem5  37570  poimirlem15  37580  poimirlem16  37581  poimirlem17  37582  poimirlem19  37584  poimirlem20  37585  poimirlem22  37587  poimirlem24  37589  poimirlem28  37593  evlselv  42535  fphpd  42764  monotuz  42890  oddcomabszz  42893  fnwe2val  42998  fnwe2lem1  42999  dfswapf2  48984  dfinito4  49171