Theorem csbeq12dv 3856

Description: Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023.)

Hypotheses

Ref	Expression
csbeq12dv.1	⊢ (𝜑 → 𝐴 = 𝐶)
csbeq12dv.2	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

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

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem csbeq12dv

Step	Hyp	Ref	Expression
1		csbeq12dv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
2	1	csbeq1d 3851	. 2 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐵)
3		csbeq12dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	3	csbeq2dv 3854	. 2 ⊢ (𝜑 → ⦋𝐶 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷)
5	2, 4	eqtrd 2795	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⦋csb 3847

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3740  df-csb 3848

This theorem is used by:  bpolylem  16167  rhmval0  20652  selvffval  22374  selvfval  22375  selvval  22376  cbvitgv  26044  mulsval  28414  precsexlemcbv  28511  precsexlem3  28514  ttgval  29371  nmulprop  36855  itgeq12sdv  36924  cbvitgvw2  36953  cbvitgdavw  36986  cbvitgdavw2  37002  poimirlem16  38468  poimirlem17  38469  poimirlem19  38471  poimirlem20  38472  isprimroot  43057  fmpocos  43201  grtri  48954  dfswapf2  50285  dfinito4  50525