Theorem csbied 3526

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ⦋csb 3499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-sbc 3403  df-csb 3500

This theorem is referenced by:  csbied2  3527  fvmptd  6197  el2mpt2cl  7138  mpt2sn  7155  cantnfval  8448  fprodeq0  14544  imasval  15994  gsumvalx  17093  mulgfval  17365  isga  17547  symgval  17622  gexval  17816  telgsumfz  18210  telgsumfz0  18212  telgsum  18214  isirred  18522  psrval  19183  mplval  19249  opsrval  19295  evlsval  19340  evls1fval  19505  evl1fval  19513  znval  19702  scmatval  20129  pmatcollpw3lem  20407  pm2mpval  20419  pm2mpmhmlem2  20443  chfacffsupp  20480  tsmsval2  21743  dvfsumle  23588  dvfsumabs  23590  dvfsumlem1  23593  dvfsum2  23601  itgparts  23614  q1pval  23717  r1pval  23720  rlimcnp2  24493  vmaval  24639  fsumdvdscom  24711  fsumvma  24738  logexprlim  24750  dchrval  24759  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  ttgval  25555  msrval  30689  poimirlem1  32580  poimirlem2  32581  poimirlem6  32585  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem23  32602  poimirlem24  32603  fsumshftd  33255  fsumshftdOLD  33256  hlhilset  36244  mendval  36772  rspc2vd  41437  ply1mulgsumlem3  41970  ply1mulgsumlem4  41971  ply1mulgsum  41972  dmatALTval  41983