MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brdif Unicode version

Theorem brdif 4502
Description: The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
Assertion
Ref Expression
brdif

Proof of Theorem brdif
StepHypRef Expression
1 eldif 3485 . 2
2 df-br 4453 . 2
3 df-br 4453 . . 3
4 df-br 4453 . . . 4
54notbii 296 . . 3
63, 5anbi12i 697 . 2
71, 2, 63bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  /\wa 369  e.wcel 1818  \cdif 3472  <.cop 4035   class class class wbr 4452
This theorem is referenced by:  fndmdif  5991  isocnv3  6228  brdifun  7357  dfsup2OLD  7923  dflt2  11383  pltval  15590  ltgov  23983  opeldifid  27456  qtophaus  27839  dftr6  29179  dffr5  29182  fundmpss  29196  brsset  29539  dfon3  29542  brtxpsd2  29545  dffun10  29564  elfuns  29565  dfrdg4  29600  dfint3  29602  brub  29604  broutsideof  29771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-br 4453
  Copyright terms: Public domain W3C validator