Theorem csbied 3864

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.)

Hypotheses

Ref	Expression
csbied.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
csbied.2	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
csbied	⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem csbied

Step	Hyp	Ref	Expression
1		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜑
2		nfcvd 2956	. 2 ⊢ (𝜑 → Ⅎ𝑥𝐶)
3		csbied.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		csbied.2	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
5	1, 2, 3, 4	csbiedf 3858	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-sbc 3721  df-csb 3829

This theorem is referenced by:  csbied2  3865  rspc2vd  3877  el2mpocl  7764  mposn  7781  cantnfval  9115  fprodeq0  15321  imasval  16776  gsumvalx  17878  efmnd  18027  mulgfval  18218  mulgfvalALT  18219  isga  18413  gexval  18695  telgsumfz  19103  telgsumfz0  19105  telgsum  19107  isirred  19445  znval  20227  psrval  20600  mplval  20666  opsrval  20714  evlsval  20758  evls1fval  20943  evl1fval  20952  scmatval  21109  pmatcollpw3lem  21388  pm2mpval  21400  pm2mpmhmlem2  21424  chfacffsupp  21461  tsmsval2  22735  dvfsumle  24624  dvfsumabs  24626  dvfsumlem1  24629  dvfsum2  24637  itgparts  24650  q1pval  24754  r1pval  24757  rlimcnp2  25552  vmaval  25698  fsumdvdscom  25770  fsumvma  25797  logexprlim  25809  dchrval  25818  dchrisumlema  26072  dchrisumlem2  26074  dchrisumlem3  26075  ttgval  26669  finsumvtxdg2sstep  27339  idlsrgval  31056  rprmval  31072  msrval  32898  poimirlem1  35058  poimirlem2  35059  poimirlem6  35063  poimirlem7  35064  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem23  35080  poimirlem24  35081  fsumshftd  36248  hlhilset  39230  prjspval  39597  mendval  40127  ply1mulgsumlem3  44796  ply1mulgsumlem4  44797  ply1mulgsum  44798  dmatALTval  44809