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

Theorem csbeq12dv 3917
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 3912 . 2 (𝜑𝐴 / 𝑥𝐵 = 𝐶 / 𝑥𝐵)
3 csbeq12dv.2 . . 3 (𝜑𝐵 = 𝐷)
43csbeq2dv 3915 . 2 (𝜑𝐶 / 𝑥𝐵 = 𝐶 / 𝑥𝐷)
52, 4eqtrd 2775 1 (𝜑𝐴 / 𝑥𝐵 = 𝐶 / 𝑥𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  csb 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792  df-csb 3909
This theorem is referenced by:  bpolylem  16081  selvffval  22155  selvfval  22156  selvval  22157  cbvitgv  25827  mulsval  28150  precsexlemcbv  28245  precsexlem3  28248  ttgval  28898  itgeq12sdv  36202  cbvitgvw2  36231  cbvitgdavw  36264  cbvitgdavw2  36280  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  isprimroot  42075  fmpocos  42254  grtri  47845
  Copyright terms: Public domain W3C validator