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

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

Proof of Theorem brin
StepHypRef Expression
1 elin 3686 . 2
2 df-br 4453 . 2
3 df-br 4453 . . 3
4 df-br 4453 . . 3
53, 4anbi12i 697 . 2
61, 2, 53bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  e.wcel 1818  i^icin 3474  <.cop 4035   class class class wbr 4452
This theorem is referenced by:  brinxp2  5066  trin2  5395  poirr2  5396  tpostpos  6994  erinxp  7404  sbthcl  7659  infxpenlem  8412  fpwwe2lem12  9040  fpwwe2  9042  isinv  15154  isffth2  15285  ffthf1o  15288  ffthoppc  15293  ffthres2c  15309  isunit  17306  opsrtoslem2  18149  posrasymb  27645  trleile  27654  dfpo2  29184  brtxp  29530  idsset  29540  dfon3  29542  elfix  29553  dffix2  29555  brcap  29590  funpartlem  29592  trer  30134  fneval  30170
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-in 3482  df-br 4453
  Copyright terms: Public domain W3C validator