Theorem csbie 3920

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 2979	. 2 ⊢ Ⅎ𝑥𝐶
3		csbie.2	. 2 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4	1, 2, 3	csbief 3919	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3496  ⦋csb 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-sbc 3775  df-csb 3886

This theorem is referenced by:  pofun  5493  eqerlem  8325  mptnn0fsuppd  13369  fsum  15079  fsumcnv  15130  fsumshftm  15138  fsum0diag2  15140  fprod  15297  fprodcnv  15339  bpolyval  15405  ruclem1  15586  odfval  18662  odval  18664  psrass1lem  20159  selvval  20333  mamufval  20998  pm2mpval  21405  isibl  24368  dfitg  24372  dvfsumlem2  24626  fsumdvdsmul  25774  disjxpin  30340  poimirlem1  34895  poimirlem5  34899  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem22  34916  poimirlem24  34918  poimirlem28  34922  fphpd  39420  monotuz  39545  oddcomabszz  39548  fnwe2val  39656  fnwe2lem1  39657