Theorem csbeq12dv 3860

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 3855	. 2 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐵)
3		csbeq12dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	3	csbeq2dv 3858	. 2 ⊢ (𝜑 → ⦋𝐶 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷)
5	2, 4	eqtrd 2764	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷)

Syntax hints:   → wi 4   = wceq 1540  ⦋csb 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3743  df-csb 3852

This theorem is referenced by:  bpolylem  15955  selvffval  22018  selvfval  22019  selvval  22020  cbvitgv  25676  mulsval  28019  precsexlemcbv  28115  precsexlem3  28118  ttgval  28824  itgeq12sdv  36213  cbvitgvw2  36242  cbvitgdavw  36275  cbvitgdavw2  36291  poimirlem16  37636  poimirlem17  37637  poimirlem19  37639  poimirlem20  37640  isprimroot  42086  fmpocos  42227  grtri  47944  dfswapf2  49266  dfinito4  49506