MPE Home 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  |-  ( A ( R  i^i  S
) B  <->  ( A R B  /\  A S B ) )

Proof of Theorem brin
StepHypRef Expression
1 elin 3639 . 2  |-  ( <. A ,  B >.  e.  ( R  i^i  S
)  <->  ( <. A ,  B >.  e.  R  /\  <. A ,  B >.  e.  S ) )
2 df-br 4393 . 2  |-  ( A ( R  i^i  S
) B  <->  <. A ,  B >.  e.  ( R  i^i  S ) )
3 df-br 4393 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4393 . . 3  |-  ( A S B  <->  <. A ,  B >.  e.  S )
53, 4anbi12i 697 . 2  |-  ( ( A R B  /\  A S B )  <->  ( <. A ,  B >.  e.  R  /\  <. A ,  B >.  e.  S ) )
61, 2, 53bitr4i 277 1  |-  ( A ( R  i^i  S
) B  <->  ( A R B  /\  A S B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1758    i^i 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