Theorem csbie 3900

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2708  Vcvv 3450  [wsbc 3756  ⦋csb 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3757  df-csb 3866

This theorem is referenced by:  pofun  5567  eqerlem  8709  mptnn0fsuppd  13970  fsum  15693  fsumcnv  15746  fsumshftm  15754  fsum0diag2  15756  fprod  15914  fprodcnv  15956  bpolyval  16022  ruclem1  16206  odfval  19469  odval  19471  psrass1lem  21848  selvval  22029  mamufval  22286  pm2mpval  22689  isibl  25673  dfitg  25677  dvfsumlem2  25940  dvfsumlem2OLD  25941  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  precsexlem3  28118  disjxpin  32524  poimirlem1  37622  poimirlem5  37626  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem24  37645  poimirlem28  37649  evlselv  42582  fphpd  42811  monotuz  42937  oddcomabszz  42940  fnwe2val  43045  fnwe2lem1  43046  dfswapf2  49254  dfinito4  49494