Theorem csbied 3892

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 3857	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbied.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		csbied.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
4	3	eleq2d 2852	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
5	2, 4	sbcied 3790	. . . . 5 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
6	5	alrimiv 1960	. . . 4 ⊢ (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
7		df-clab 2745	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵)
8		eleq1w 2849	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	8	sbcbidv 3802	. . . . . . . 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 2759	. . 3 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
16	14, 15	sylibr 237	. 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶)
17	1, 16	eqtrid 2813	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-sbc 3748  df-csb 3857

This theorem is used by:  csbied2  3893  rspc2vd  3904  el2mpocl  8090  mposn  8107  cantnfval  9647  fprodeq0  16055  imasval  17590  gsumvalx  18763  efmnd  18960  mulgfval  19166  mulgfvalALT  19167  isga  19392  gexval  19679  telgsumfz  20091  telgsumfz0  20093  telgsum  20095  isirred  20534  znval  21722  psrval  22102  mplval  22175  opsrval  22234  evlsval  22274  evls1fval  22516  evl1fval  22525  scmatval  22698  pmatcollpw3lem  22977  pm2mpval  22989  pm2mpmhmlem2  23013  chfacffsupp  23050  tsmsval2  24324  dvfsumle  26217  dvfsumabs  26219  dvfsumlem1  26222  dvfsum2  26230  itgparts  26243  q1pval  26349  r1pval  26352  rlimcnp2  27168  vmaval  27314  fsumdvdscom  27386  fsumvma  27414  logexprlim  27426  dchrval  27435  dchrisumlema  27689  dchrisumlem2  27691  dchrisumlem3  27692  mulsval  28339  ttgval  29261  finsumvtxdg2sstep  29936  gsummptp1  33408  gsummptfzsplitra  33409  gsummptfzsplitla  33410  gsummulsubdishift1s  33421  gsummulsubdishift2s  33422  idlsrgval  33824  rprmval  33837  gsummoncoe1fzo  33918  msrval  36051  poimirlem1  38313  poimirlem2  38314  poimirlem6  38318  poimirlem7  38319  poimirlem10  38322  poimirlem11  38323  poimirlem12  38324  poimirlem23  38335  poimirlem24  38336  fsumshftd  39767  hlhilset  42749  isprimroot  42901  prjspval  43376  mendval  43947  isisubgr  48668  ply1mulgsumlem3  49209  ply1mulgsumlem4  49210  ply1mulgsum  49211  dmatALTval  49221  dfinito4  50320