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

Theorem brin 4441
 Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
Assertion
Ref Expression
brin

Proof of Theorem brin
StepHypRef Expression
1 elin 3639 . 2
2 df-br 4393 . 2
3 df-br 4393 . . 3
4 df-br 4393 . . 3
53, 4anbi12i 697 . 2
61, 2, 53bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wa 369   wcel 1758   cin 3427  cop 3983   class class class wbr 4392 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-in 3435  df-br 4393 This theorem is referenced by:  brinxp2  5000  trin2  5321  poirr2  5322  tpostpos  6867  erinxp  7276  sbthcl  7535  infxpenlem  8283  fpwwe2lem12  8911  fpwwe2  8913  isinv  14802  isffth2  14930  ffthf1o  14933  ffthoppc  14938  ffthres2c  14954  isunit  16857  opsrtoslem2  17675  posrasymb  26254  trleile  26263  dfpo2  27701  brtxp  28047  idsset  28057  dfon3  28059  elfix  28070  dffix2  28072  brcap  28107  funpartlem  28109  trer  28651  fneval  28699  fnessref  28705  refssfne  28706
 Copyright terms: Public domain W3C validator