Theorem csbie 3916

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

Syntax hints:   → wi 4   = wceq 1531   ∈ wcel 2108  Vcvv 3493  ⦋csb 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-sbc 3771  df-csb 3882

This theorem is referenced by:  pofun  5484  eqerlem  8315  mptnn0fsuppd  13358  fsum  15069  fsumcnv  15120  fsumshftm  15128  fsum0diag2  15130  fprod  15287  fprodcnv  15329  bpolyval  15395  ruclem1  15576  odfval  18652  odval  18654  psrass1lem  20149  selvval  20323  mamufval  20988  pm2mpval  21395  isibl  24358  dfitg  24362  dvfsumlem2  24616  fsumdvdsmul  25764  disjxpin  30330  poimirlem1  34885  poimirlem5  34889  poimirlem15  34899  poimirlem16  34900  poimirlem17  34901  poimirlem19  34903  poimirlem20  34904  poimirlem22  34906  poimirlem24  34908  poimirlem28  34912  fphpd  39403  monotuz  39528  oddcomabszz  39531  fnwe2val  39639  fnwe2lem1  39640