Theorem csbied 3888

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 3853	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		csbied.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		csbied.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
4	3	eleq2d 2847	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
5	2, 4	sbcied 3787	. . . . 5 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
6	5	alrimiv 1946	. . . 4 ⊢ (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
7		df-clab 2740	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵)
8		eleq1w 2844	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	8	sbcbidv 3799	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵))
10	9	sbievw 2126	. . . . . . 7 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵)
11	7, 10	bitr2i 278	. . . . . 6 ⊢ ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵})
12	11	bibi1i 340	. . . . 5 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) ↔ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
13	12	biimpi 218	. . . 4 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) → (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
14	6, 13	sylg 1842	. . 3 ⊢ (𝜑 → ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
15		dfcleq 2754	. . 3 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶))
16	14, 15	sylibr 236	. 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶)
17	1, 16	eqtrid 2808	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   = wceq 1559  [wsb 2089   ∈ wcel 2141  {cab 2739  [wsbc 3744  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3745  df-csb 3853

This theorem is referenced by:  csbied2  3889  rspc2vd  3900  el2mpocl  8060  mposn  8077  cantnfval  9620  fprodeq0  15988  imasval  17524  gsumvalx  18693  efmnd  18887  mulgfval  19094  mulgfvalALT  19095  isga  19314  gexval  19601  telgsumfz  20013  telgsumfz0  20015  telgsum  20017  isirred  20447  znval  21567  psrval  21947  mplval  22020  opsrval  22079  evlsval  22119  evls1fval  22362  evl1fval  22371  scmatval  22544  pmatcollpw3lem  22823  pm2mpval  22835  pm2mpmhmlem2  22859  chfacffsupp  22896  tsmsval2  24170  dvfsumle  26063  dvfsumabs  26065  dvfsumlem1  26068  dvfsum2  26076  itgparts  26089  q1pval  26195  r1pval  26198  rlimcnp2  27008  vmaval  27154  fsumdvdscom  27226  fsumvma  27254  logexprlim  27266  dchrval  27275  dchrisumlema  27529  dchrisumlem2  27531  dchrisumlem3  27532  mulsval  28179  ttgval  29021  finsumvtxdg2sstep  29696  gsummptp1  33198  gsummptfzsplitra  33199  gsummptfzsplitla  33200  gsummulsubdishift1s  33211  gsummulsubdishift2s  33212  idlsrgval  33660  rprmval  33673  gsummoncoe1fzo  33754  msrval  35852  poimirlem1  38084  poimirlem2  38085  poimirlem6  38089  poimirlem7  38090  poimirlem10  38093  poimirlem11  38094  poimirlem12  38095  poimirlem23  38106  poimirlem24  38107  fsumshftd  39540  hlhilset  42522  isprimroot  42674  prjspval  43149  mendval  43720  isisubgr  48448  ply1mulgsumlem3  48974  ply1mulgsumlem4  48975  ply1mulgsum  48976  dmatALTval  48986  dfinito4  50086