Theorem csbie 3922

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) Reduce axiom usage. (Revised by Gino Giotto, 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 3887	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbie.1	. . . 4 ⊢ 𝐴 ∈ V
3		csbie.2	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	3	eleq2d 2811	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
5	2, 4	sbcie 3813	. . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)
6	5	abbii 2794	. 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶}
7		abid2 2863	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶
8	1, 6, 7	3eqtri 2756	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  {cab 2701  Vcvv 3466  [wsbc 3770  ⦋csb 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-sbc 3771  df-csb 3887

This theorem is referenced by:  pofun  5597  eqerlem  8734  mptnn0fsuppd  13961  fsum  15664  fsumcnv  15717  fsumshftm  15725  fsum0diag2  15727  fprod  15883  fprodcnv  15925  bpolyval  15991  ruclem1  16173  odfval  19444  odval  19446  psrass1lemOLD  21804  psrass1lem  21807  selvval  21990  mamufval  22211  pm2mpval  22621  isibl  25619  dfitg  25623  dvfsumlem2  25885  dvfsumlem2OLD  25886  fsumdvdsmul  27046  fsumdvdsmulOLD  27048  precsexlem3  28026  disjxpin  32291  poimirlem1  36983  poimirlem5  36987  poimirlem15  36997  poimirlem16  36998  poimirlem17  36999  poimirlem19  37001  poimirlem20  37002  poimirlem22  37004  poimirlem24  37006  poimirlem28  37010  evlselv  41652  fphpd  42068  monotuz  42194  oddcomabszz  42197  fnwe2val  42305  fnwe2lem1  42306