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 2850	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
5	2, 4	sbcie 3783	. . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)
6	5	abbii 2830	. 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶}
7		abid2 2901	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶
8	1, 6, 7	3eqtri 2790	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {cab 2741  Vcvv 3454  [wsbc 3742  ⦋csb 3851

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743  df-csb 3852

This theorem is used by:  pofun  5581  fnwe2lem1  8172  fnwe2lem2  8173  eqerlem  8781  mptnn0fsuppd  14168  fsum  15915  fsumcnv  15968  fsumshftm  15976  fsum0diag2  15978  fprod  16137  fprodcnv  16179  bpolyval  16244  ruclem1  16428  odfval  19776  odval  19778  psrass1lem  22271  selvval  22459  mamufval  22737  pm2mpval  23143  isibl  26116  dfitg  26120  dvfsumlem2  26377  fsumdvdsmul  27552  precsexlem3  28625  disjxpin  33254  gsummulsubdishift2s  33702  nmulprop  37117  poimirlem1  38731  poimirlem5  38735  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem22  38752  poimirlem24  38754  poimirlem28  38758  evlselv  43810  fphpd  44016  monotuz  44141  oddcomabszz  44144  dfswapf2  50588  dfinito4  50841