Theorem csbie 3825

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.)

Hypotheses

Ref	Expression
csbie.1	⊢ 𝐴 ∈ V
csbie.2	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
csbie	⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem csbie

Step	Hyp	Ref	Expression
1		csbie.1	. 2 ⊢ 𝐴 ∈ V
2		nfcv 2899	. 2 ⊢ Ⅎ𝑥𝐶
3		csbie.2	. 2 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	1, 2, 3	csbief 3824	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3398  ⦋csb 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-v 3400  df-sbc 3681  df-csb 3791

This theorem is referenced by:  pofun  5460  eqerlem  8356  mptnn0fsuppd  13459  fsum  15172  fsumcnv  15223  fsumshftm  15231  fsum0diag2  15233  fprod  15389  fprodcnv  15431  bpolyval  15497  ruclem1  15678  odfval  18780  odval  18782  psrass1lemOLD  20755  psrass1lem  20758  selvval  20934  mamufval  21140  pm2mpval  21548  isibl  24520  dfitg  24524  dvfsumlem2  24781  fsumdvdsmul  25934  disjxpin  30503  poimirlem1  35423  poimirlem5  35427  poimirlem15  35437  poimirlem16  35438  poimirlem17  35439  poimirlem19  35441  poimirlem20  35442  poimirlem22  35444  poimirlem24  35446  poimirlem28  35450  fphpd  40232  monotuz  40357  oddcomabszz  40360  fnwe2val  40468  fnwe2lem1  40469