Theorem csbie 3881

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 3847	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbie.1	. . . 4 ⊢ 𝐴 ∈ V
3		csbie.2	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	3	eleq2d 2846	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
5	2, 4	sbcie 3779	. . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)
6	5	abbii 2827	. 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶}
7		abid2 2897	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶
8	1, 6, 7	3eqtri 2787	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {cab 2738  Vcvv 3450  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  pofun  5576  fnwe2lem1  8145  fnwe2lem2  8146  eqerlem  8754  mptnn0fsuppd  14142  fsum  15887  fsumcnv  15940  fsumshftm  15948  fsum0diag2  15950  fprod  16109  fprodcnv  16151  bpolyval  16216  ruclem1  16400  odfval  19747  odval  19749  psrass1lem  22242  selvval  22430  mamufval  22708  pm2mpval  23114  isibl  26087  dfitg  26091  dvfsumlem2  26348  fsumdvdsmul  27523  precsexlem3  28596  disjxpin  33225  gsummulsubdishift2s  33675  nmulprop  37014  poimirlem1  38615  poimirlem5  38619  poimirlem15  38629  poimirlem16  38630  poimirlem17  38631  poimirlem19  38633  poimirlem20  38634  poimirlem22  38636  poimirlem24  38638  poimirlem28  38642  evlselv  43693  fphpd  43899  monotuz  44024  oddcomabszz  44027  dfswapf2  50445  dfinito4  50685