Theorem csbied 3778

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 1957	. 2 ⊢ Ⅎ𝑥𝜑
2		nfcvd 2935	. 2 ⊢ (𝜑 → Ⅎ𝑥𝐶)
3		csbied.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4		csbied.2	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
5	1, 2, 3, 4	csbiedf 3772	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  ⦋csb 3751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-sbc 3653  df-csb 3752

This theorem is referenced by:  csbied2  3779  fvmptd  6548  el2mpt2cl  7531  mpt2sn  7549  cantnfval  8862  fprodeq0  15108  imasval  16557  gsumvalx  17656  mulgfval  17929  isga  18107  symgval  18182  gexval  18377  telgsumfz  18774  telgsumfz0  18776  telgsum  18778  isirred  19086  psrval  19759  mplval  19825  opsrval  19871  evlsval  19915  evls1fval  20080  evl1fval  20088  znval  20279  scmatval  20715  pmatcollpw3lem  20995  pm2mpval  21007  pm2mpmhmlem2  21031  chfacffsupp  21068  tsmsval2  22341  dvfsumle  24221  dvfsumabs  24223  dvfsumlem1  24226  dvfsum2  24234  itgparts  24247  q1pval  24350  r1pval  24353  rlimcnp2  25145  vmaval  25291  fsumdvdscom  25363  fsumvma  25390  logexprlim  25402  dchrval  25411  dchrisumlema  25629  dchrisumlem2  25631  dchrisumlem3  25632  ttgval  26224  finsumvtxdg2sstep  26897  rspc2vd  27673  msrval  32034  poimirlem1  34036  poimirlem2  34037  poimirlem6  34041  poimirlem7  34042  poimirlem10  34045  poimirlem11  34046  poimirlem12  34047  poimirlem23  34058  poimirlem24  34059  fsumshftd  35106  hlhilset  38088  prjspval  38204  mendval  38712  ply1mulgsumlem3  43191  ply1mulgsumlem4  43192  ply1mulgsum  43193  dmatALTval  43204