Theorem csbied 3560

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ⦋csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sbc 3436  df-csb 3534

This theorem is referenced by:  csbied2  3561  fvmptd  6288  el2mpt2cl  7251  mpt2sn  7268  cantnfval  8565  fprodeq0  14705  imasval  16171  gsumvalx  17270  mulgfval  17542  isga  17724  symgval  17799  gexval  17993  telgsumfz  18387  telgsumfz0  18389  telgsum  18391  isirred  18699  psrval  19362  mplval  19428  opsrval  19474  evlsval  19519  evls1fval  19684  evl1fval  19692  znval  19883  scmatval  20310  pmatcollpw3lem  20588  pm2mpval  20600  pm2mpmhmlem2  20624  chfacffsupp  20661  tsmsval2  21933  dvfsumle  23784  dvfsumabs  23786  dvfsumlem1  23789  dvfsum2  23797  itgparts  23810  q1pval  23913  r1pval  23916  rlimcnp2  24693  vmaval  24839  fsumdvdscom  24911  fsumvma  24938  logexprlim  24950  dchrval  24959  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  ttgval  25755  finsumvtxdg2sstep  26445  rspc2vd  27129  msrval  31435  poimirlem1  33410  poimirlem2  33411  poimirlem6  33415  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem23  33432  poimirlem24  33433  fsumshftd  34237  fsumshftdOLD  34238  hlhilset  37226  mendval  37753  ply1mulgsumlem3  42176  ply1mulgsumlem4  42177  ply1mulgsum  42178  dmatALTval  42189