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

Theorem brin 4070
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 3358 . 2  |-  ( <. A ,  B >.  e.  ( R  i^i  S
)  <->  ( <. A ,  B >.  e.  R  /\  <. A ,  B >.  e.  S ) )
2 df-br 4024 . 2  |-  ( A ( R  i^i  S
) B  <->  <. A ,  B >.  e.  ( R  i^i  S ) )
3 df-br 4024 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4024 . . 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 1684    i^i cin 3151   <.cop 3643   class class class wbr 4023
This theorem is referenced by:  brinxp2  4751  trin2  5066  poirr2  5067  tpostpos  6254  erinxp  6733  sbthcl  6983  infxpenlem  7641  fpwwe2lem12  8263  fpwwe2  8265  isinv  13662  isffth2  13790  ffthf1o  13793  ffthoppc  13798  ffthres2c  13814  isunit  15439  opsrtoslem2  16226  dfpo2  24112  brtxp  24420  idsset  24430  dfon3  24432  elfix  24443  dffix2  24445  brcap  24479  funpartfun  24481  funpartfv  24483  domintrefb  25063  definc  25279  trer  26227  fneval  26287  fnessref  26293  refssfne  26294
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-br 4024
  Copyright terms: Public domain W3C validator