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

Theorem difeq12i 4134
Description: Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
Hypotheses
Ref Expression
difeq1i.1 𝐴 = 𝐵
difeq12i.2 𝐶 = 𝐷
Assertion
Ref Expression
difeq12i (𝐴𝐶) = (𝐵𝐷)

Proof of Theorem difeq12i
StepHypRef Expression
1 difeq1i.1 . . 3 𝐴 = 𝐵
21difeq1i 4132 . 2 (𝐴𝐶) = (𝐵𝐶)
3 difeq12i.2 . . 3 𝐶 = 𝐷
43difeq2i 4133 . 2 (𝐵𝐶) = (𝐵𝐷)
52, 4eqtri 2763 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  cdif 3960
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-rab 3434  df-dif 3966
This theorem is referenced by:  indifdir  4301  difrab  4324  resdifdi  6258  resdifdir  6259  preddif  6352  infdju1  10228  uniioombllem4  25635  new0  27928  clwwlknclwwlkdif  30008  gtiso  32716  satffunlem2lem2  35391  mthmpps  35567  zrdivrng  37940  isdrngo1  37943  pwfi2f1o  43085  salexct2  46295  dfnelbr2  47223
  Copyright terms: Public domain W3C validator