Theorem csbie 3883

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 3849	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbie.1	. . . 4 ⊢ 𝐴 ∈ V
3		csbie.2	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	3	eleq2d 2815	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
5	2, 4	sbcie 3781	. . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)
6	5	abbii 2797	. 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶}
7		abid2 2866	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶
8	1, 6, 7	3eqtri 2757	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  {cab 2708  Vcvv 3434  [wsbc 3739  ⦋csb 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3740  df-csb 3849

This theorem is referenced by:  pofun  5540  eqerlem  8652  mptnn0fsuppd  13897  fsum  15619  fsumcnv  15672  fsumshftm  15680  fsum0diag2  15682  fprod  15840  fprodcnv  15882  bpolyval  15948  ruclem1  16132  odfval  19437  odval  19439  psrass1lem  21862  selvval  22043  mamufval  22300  pm2mpval  22703  isibl  25686  dfitg  25690  dvfsumlem2  25953  dvfsumlem2OLD  25954  fsumdvdsmul  27125  fsumdvdsmulOLD  27127  precsexlem3  28140  disjxpin  32558  poimirlem1  37640  poimirlem5  37644  poimirlem15  37654  poimirlem16  37655  poimirlem17  37656  poimirlem19  37658  poimirlem20  37659  poimirlem22  37661  poimirlem24  37663  poimirlem28  37667  evlselv  42599  fphpd  42828  monotuz  42953  oddcomabszz  42956  fnwe2val  43061  fnwe2lem1  43062  dfswapf2  49272  dfinito4  49512