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

Theorem difeq12i 4081
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 4079 . 2 (𝐴𝐶) = (𝐵𝐶)
3 difeq12i.2 . . 3 𝐶 = 𝐷
43difeq2i 4080 . 2 (𝐵𝐶) = (𝐵𝐷)
52, 4eqtri 2761 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cdif 3908
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 3407  df-dif 3914
This theorem is referenced by:  indifdir  4245  difrab  4269  resdifdi  6189  resdifdir  6190  preddif  6284  infdju1  10130  uniioombllem4  24966  new0  27226  clwwlknclwwlkdif  28965  gtiso  31661  satffunlem2lem2  34057  mthmpps  34233  zrdivrng  36458  isdrngo1  36461  pwfi2f1o  41466  salexct2  44666  dfnelbr2  45591
  Copyright terms: Public domain W3C validator