Theorem csbied 3882

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 3847	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbied.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		csbied.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
4	3	eleq2d 2846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
5	2, 4	sbcied 3781	. . . . 5 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
6	5	alrimiv 1959	. . . 4 ⊢ (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
7		df-clab 2739	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵)
8		eleq1w 2843	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	8	sbcbidv 3793	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵))
10	9	sbievw 2130	. . . . . . 7 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵)
11	7, 10	bitr2i 279	. . . . . 6 ⊢ ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵})
12	11	bibi1i 341	. . . . 5 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) ↔ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
13	12	biimpi 219	. . . 4 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) → (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
14	6, 13	sylg 1855	. . 3 ⊢ (𝜑 → ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
15		dfcleq 2753	. . 3 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
16	14, 15	sylibr 237	. 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶)
17	1, 16	eqtrid 2807	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  [wsb 2098   ∈ wcel 2144  {cab 2738  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbied2  3883  rspc2vd  3894  el2mpocl  8097  mposn  8116  cantnfval  9672  fprodeq0  16147  imasval  17688  gsumvalx  18870  efmnd  19071  mulgfval  19284  mulgfvalALT  19285  isga  19510  gexval  19797  telgsumfz  20209  telgsumfz0  20211  telgsum  20213  isirred  20654  znval  21846  psrval  22228  mplval  22301  opsrval  22360  evlsval  22400  evls1fval  22642  evl1fval  22651  scmatval  22824  pmatcollpw3lem  23106  pm2mpval  23118  pm2mpmhmlem2  23142  chfacffsupp  23179  tsmsval2  24454  dvfsumle  26346  dvfsumabs  26348  dvfsumlem1  26351  dvfsum2  26359  itgparts  26372  q1pval  26478  r1pval  26481  rlimcnp2  27299  vmaval  27445  fsumdvdscom  27517  fsumvma  27545  logexprlim  27557  dchrval  27566  dchrisumlema  27820  dchrisumlem2  27822  dchrisumlem3  27823  mulsval  28500  ttgval  29457  finsumvtxdg2sstep  30135  gsummptp1  33664  gsummptfzsplitra  33665  gsummptfzsplitla  33666  gsummulsubdishift1s  33677  gsummulsubdishift2s  33678  idlsrgval  34081  rprmval  34094  gsummoncoe1fzo  34175  msrval  36389  poimirlem1  38632  poimirlem2  38633  poimirlem6  38637  poimirlem7  38638  poimirlem10  38641  poimirlem11  38642  poimirlem12  38643  poimirlem23  38654  poimirlem24  38655  fsumshftd  40102  hlhilset  43084  isprimroot  43236  prjspval  43724  mendval  44274  isisubgr  49053  ply1mulgsumlem3  49593  ply1mulgsumlem4  49594  ply1mulgsum  49595  dmatALTval  49605  dfinito4  50729