Theorem csbied 3890

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 3855	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbied.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		csbied.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
4	3	eleq2d 2849	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
5	2, 4	sbcied 3788	. . . . 5 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
6	5	alrimiv 1957	. . . 4 ⊢ (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
7		df-clab 2742	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵)
8		eleq1w 2846	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	8	sbcbidv 3800	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵))
10	9	sbievw 2128	. . . . . . 7 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵)
11	7, 10	bitr2i 279	. . . . . 6 ⊢ ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵})
12	11	bibi1i 341	. . . . 5 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) ↔ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
13	12	biimpi 219	. . . 4 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) → (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
14	6, 13	sylg 1853	. . 3 ⊢ (𝜑 → ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
15		dfcleq 2756	. . 3 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
16	14, 15	sylibr 237	. 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶)
17	1, 16	eqtrid 2810	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570  [wsb 2096   ∈ wcel 2143  {cab 2741  [wsbc 3745  ⦋csb 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746  df-csb 3855

This theorem is referenced by:  csbied2  3891  rspc2vd  3902  el2mpocl  8082  mposn  8099  cantnfval  9638  fprodeq0  16031  imasval  17566  gsumvalx  18735  efmnd  18930  mulgfval  19136  mulgfvalALT  19137  isga  19362  gexval  19649  telgsumfz  20061  telgsumfz0  20063  telgsum  20065  isirred  20502  znval  21666  psrval  22046  mplval  22119  opsrval  22178  evlsval  22218  evls1fval  22460  evl1fval  22469  scmatval  22642  pmatcollpw3lem  22921  pm2mpval  22933  pm2mpmhmlem2  22957  chfacffsupp  22994  tsmsval2  24268  dvfsumle  26161  dvfsumabs  26163  dvfsumlem1  26166  dvfsum2  26174  itgparts  26187  q1pval  26293  r1pval  26296  rlimcnp2  27112  vmaval  27258  fsumdvdscom  27330  fsumvma  27358  logexprlim  27370  dchrval  27379  dchrisumlema  27633  dchrisumlem2  27635  dchrisumlem3  27636  mulsval  28283  ttgval  29205  finsumvtxdg2sstep  29880  gsummptp1  33358  gsummptfzsplitra  33359  gsummptfzsplitla  33360  gsummulsubdishift1s  33371  gsummulsubdishift2s  33372  idlsrgval  33774  rprmval  33787  gsummoncoe1fzo  33868  msrval  36011  poimirlem1  38253  poimirlem2  38254  poimirlem6  38258  poimirlem7  38259  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem23  38275  poimirlem24  38276  fsumshftd  39707  hlhilset  42689  isprimroot  42841  prjspval  43318  mendval  43889  isisubgr  48610  ply1mulgsumlem3  49151  ply1mulgsumlem4  49152  ply1mulgsum  49153  dmatALTval  49163  dfinito4  50262