Theorem csbied 3886

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.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.)

Hypotheses

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

Assertion

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

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

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

Proof of Theorem csbied

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-csb 3851	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbied.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		csbied.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
4	3	eleq2d 2848	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
5	2, 4	sbcied 3785	. . . . 5 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
6	5	alrimiv 1960	. . . 4 ⊢ (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
7		df-clab 2741	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵)
8		eleq1w 2845	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	8	sbcbidv 3797	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵))
10	9	sbievw 2131	. . . . . . 7 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵)
11	7, 10	bitr2i 279	. . . . . 6 ⊢ ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵})
12	11	bibi1i 341	. . . . 5 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) ↔ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
13	12	biimpi 219	. . . 4 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) → (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
14	6, 13	sylg 1856	. . 3 ⊢ (𝜑 → ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
15		dfcleq 2755	. . 3 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
16	14, 15	sylibr 237	. 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶)
17	1, 16	eqtrid 2809	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  [wsb 2099   ∈ wcel 2145  {cab 2740  [wsbc 3742  ⦋csb 3850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743  df-csb 3851

This theorem is used by:  csbied2  3887  rspc2vd  3898  el2mpocl  8087  mposn  8104  cantnfval  9651  fprodeq0  16068  imasval  17603  gsumvalx  18784  efmnd  18985  mulgfval  19198  mulgfvalALT  19199  isga  19424  gexval  19711  telgsumfz  20123  telgsumfz0  20125  telgsum  20127  isirred  20566  znval  21754  psrval  22136  mplval  22209  opsrval  22268  evlsval  22308  evls1fval  22550  evl1fval  22559  scmatval  22732  pmatcollpw3lem  23014  pm2mpval  23026  pm2mpmhmlem2  23050  chfacffsupp  23087  tsmsval2  24362  dvfsumle  26255  dvfsumabs  26257  dvfsumlem1  26260  dvfsum2  26268  itgparts  26281  q1pval  26387  r1pval  26390  rlimcnp2  27211  vmaval  27357  fsumdvdscom  27429  fsumvma  27457  logexprlim  27469  dchrval  27478  dchrisumlema  27732  dchrisumlem2  27734  dchrisumlem3  27735  mulsval  28382  ttgval  29339  finsumvtxdg2sstep  30017  gsummptp1  33505  gsummptfzsplitra  33506  gsummptfzsplitla  33507  gsummulsubdishift1s  33518  gsummulsubdishift2s  33519  idlsrgval  33921  rprmval  33934  gsummoncoe1fzo  34015  msrval  36125  poimirlem1  38378  poimirlem2  38379  poimirlem6  38383  poimirlem7  38384  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem23  38400  poimirlem24  38401  fsumshftd  39833  hlhilset  42815  isprimroot  42967  prjspval  43457  mendval  44028  isisubgr  48786  ply1mulgsumlem3  49326  ply1mulgsumlem4  49327  ply1mulgsum  49328  dmatALTval  49338  dfinito4  50435