Theorem csbied 3593

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ⦋csb 3566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sbc 3469  df-csb 3567

This theorem is referenced by:  csbied2  3594  fvmptd  6327  el2mpt2cl  7296  mpt2sn  7313  cantnfval  8603  fprodeq0  14749  imasval  16218  gsumvalx  17317  mulgfval  17589  isga  17770  symgval  17845  gexval  18039  telgsumfz  18433  telgsumfz0  18435  telgsum  18437  isirred  18745  psrval  19410  mplval  19476  opsrval  19522  evlsval  19567  evls1fval  19732  evl1fval  19740  znval  19931  scmatval  20358  pmatcollpw3lem  20636  pm2mpval  20648  pm2mpmhmlem2  20672  chfacffsupp  20709  tsmsval2  21980  dvfsumle  23829  dvfsumabs  23831  dvfsumlem1  23834  dvfsum2  23842  itgparts  23855  q1pval  23958  r1pval  23961  rlimcnp2  24738  vmaval  24884  fsumdvdscom  24956  fsumvma  24983  logexprlim  24995  dchrval  25004  dchrisumlema  25222  dchrisumlem2  25224  dchrisumlem3  25225  ttgval  25800  finsumvtxdg2sstep  26501  rspc2vd  27245  msrval  31561  poimirlem1  33540  poimirlem2  33541  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem23  33562  poimirlem24  33563  fsumshftd  34556  hlhilset  37543  mendval  38070  ply1mulgsumlem3  42501  ply1mulgsumlem4  42502  ply1mulgsum  42503  dmatALTval  42514