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

Theorem brin 4172
Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
Assertion
Ref Expression
brin  |-  ( A ( R  i^i  S
) B  <->  ( A R B  /\  A S B ) )

Proof of Theorem brin
StepHypRef Expression
1 elin 3446 . 2  |-  ( <. A ,  B >.  e.  ( R  i^i  S
)  <->  ( <. A ,  B >.  e.  R  /\  <. A ,  B >.  e.  S ) )
2 df-br 4126 . 2  |-  ( A ( R  i^i  S
) B  <->  <. A ,  B >.  e.  ( R  i^i  S ) )
3 df-br 4126 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4126 . . 3  |-  ( A S B  <->  <. A ,  B >.  e.  S )
53, 4anbi12i 678 . 2  |-  ( ( A R B  /\  A S B )  <->  ( <. A ,  B >.  e.  R  /\  <. A ,  B >.  e.  S ) )
61, 2, 53bitr4i 268 1  |-  ( A ( R  i^i  S
) B  <->  ( A R B  /\  A S B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    e. wcel 1715    i^i cin 3237   <.cop 3732   class class class wbr 4125
This theorem is referenced by:  brinxp2  4854  trin2  5169  poirr2  5170  tpostpos  6396  erinxp  6875  sbthcl  7126  infxpenlem  7788  fpwwe2lem12  8410  fpwwe2  8412  isinv  13872  isffth2  14000  ffthf1o  14003  ffthoppc  14008  ffthres2c  14024  isunit  15649  opsrtoslem2  16436  dfpo2  24853  brtxp  25161  idsset  25171  dfon3  25173  elfix  25184  dffix2  25186  brcap  25220  funpartlem  25222  trer  25734  fneval  25794  fnessref  25800  refssfne  25801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245  df-br 4126
  Copyright terms: Public domain W3C validator