Theorem csbie 3878

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  {cab 2730  Vcvv 3444  [wsbc 3735  ⦋csb 3843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-sbc 3736  df-csb 3844

This theorem is referenced by:  pofun  5562  eqerlem  8698  mptnn0fsuppd  13997  fsum  15719  fsumcnv  15772  fsumshftm  15780  fsum0diag2  15782  fprod  15943  fprodcnv  15985  bpolyval  16051  ruclem1  16235  odfval  19544  odval  19546  psrass1lem  21954  selvval  22142  mamufval  22421  pm2mpval  22824  isibl  25796  dfitg  25800  dvfsumlem2  26058  fsumdvdsmul  27225  precsexlem3  28268  disjxpin  32726  gsummulsubdishift2s  33201  nmulprop  36478  poimirlem1  38058  poimirlem5  38062  poimirlem15  38072  poimirlem16  38073  poimirlem17  38074  poimirlem19  38076  poimirlem20  38077  poimirlem22  38079  poimirlem24  38081  poimirlem28  38085  evlselv  43109  fphpd  43331  monotuz  43456  oddcomabszz  43459  fnwe2val  43564  fnwe2lem1  43565  dfswapf2  49820  dfinito4  50060