Theorem csbie 3882

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 3848	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbie.1	. . . 4 ⊢ 𝐴 ∈ V
3		csbie.2	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	3	eleq2d 2842	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
5	2, 4	sbcie 3780	. . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)
6	5	abbii 2823	. 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶}
7		abid2 2893	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶
8	1, 6, 7	3eqtri 2783	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  {cab 2734  Vcvv 3448  [wsbc 3739  ⦋csb 3847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-sbc 3740  df-csb 3848

This theorem is referenced by:  pofun  5566  eqerlem  8702  mptnn0fsuppd  14001  fsum  15723  fsumcnv  15776  fsumshftm  15784  fsum0diag2  15786  fprod  15947  fprodcnv  15989  bpolyval  16055  ruclem1  16239  odfval  19548  odval  19550  psrass1lem  21958  selvval  22146  mamufval  22425  pm2mpval  22828  isibl  25800  dfitg  25804  dvfsumlem2  26062  fsumdvdsmul  27229  precsexlem3  28272  disjxpin  32730  gsummulsubdishift2s  33205  nmulprop  36488  poimirlem1  38068  poimirlem5  38072  poimirlem15  38082  poimirlem16  38083  poimirlem17  38084  poimirlem19  38086  poimirlem20  38087  poimirlem22  38089  poimirlem24  38091  poimirlem28  38095  evlselv  43119  fphpd  43341  monotuz  43466  oddcomabszz  43469  fnwe2val  43574  fnwe2lem1  43575  dfswapf2  49830  dfinito4  50070