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

Theorem difeq12i 4121
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 4119 . 2 (𝐴𝐶) = (𝐵𝐶)
3 difeq12i.2 . . 3 𝐶 = 𝐷
43difeq2i 4120 . 2 (𝐵𝐶) = (𝐵𝐷)
52, 4eqtri 2761 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cdif 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-dif 3952
This theorem is referenced by:  indifdir  4285  difrab  4309  resdifdi  6236  resdifdir  6237  preddif  6331  infdju1  10184  uniioombllem4  25103  new0  27369  clwwlknclwwlkdif  29232  gtiso  31922  satffunlem2lem2  34397  mthmpps  34573  zrdivrng  36821  isdrngo1  36824  pwfi2f1o  41838  salexct2  45055  dfnelbr2  45981
  Copyright terms: Public domain W3C validator