MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbeq12dv Structured version   Visualization version   GIF version

Theorem csbeq12dv 3908
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
StepHypRef Expression
1 csbeq12dv.1 . . 3 (𝜑𝐴 = 𝐶)
21csbeq1d 3903 . 2 (𝜑𝐴 / 𝑥𝐵 = 𝐶 / 𝑥𝐵)
3 csbeq12dv.2 . . 3 (𝜑𝐵 = 𝐷)
43csbeq2dv 3906 . 2 (𝜑𝐶 / 𝑥𝐵 = 𝐶 / 𝑥𝐷)
52, 4eqtrd 2777 1 (𝜑𝐴 / 𝑥𝐵 = 𝐶 / 𝑥𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  csb 3899
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789  df-csb 3900
This theorem is referenced by:  bpolylem  16084  selvffval  22137  selvfval  22138  selvval  22139  cbvitgv  25812  mulsval  28135  precsexlemcbv  28230  precsexlem3  28233  ttgval  28883  itgeq12sdv  36220  cbvitgvw2  36249  cbvitgdavw  36282  cbvitgdavw2  36298  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  isprimroot  42094  fmpocos  42275  grtri  47907  dfswapf2  48967
  Copyright terms: Public domain W3C validator