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

Theorem brin 4488
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 3673 . 2  |-  ( <. A ,  B >.  e.  ( R  i^i  S
)  <->  ( <. A ,  B >.  e.  R  /\  <. A ,  B >.  e.  S ) )
2 df-br 4440 . 2  |-  ( A ( R  i^i  S
) B  <->  <. A ,  B >.  e.  ( R  i^i  S ) )
3 df-br 4440 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4440 . . 3  |-  ( A S B  <->  <. A ,  B >.  e.  S )
53, 4anbi12i 695 . 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 367    e. wcel 1823    i^i cin 3460   <.cop 4022   class class class wbr 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-br 4440
This theorem is referenced by:  brinxp2  5050  trin2  5378  poirr2  5379  tpostpos  6967  erinxp  7377  sbthcl  7632  infxpenlem  8382  fpwwe2lem12  9008  fpwwe2  9010  isinv  15248  isffth2  15404  ffthf1o  15407  ffthoppc  15412  ffthres2c  15428  isunit  17501  opsrtoslem2  18344  posrasymb  27879  trleile  27888  dfpo2  29425  brtxp  29758  idsset  29768  dfon3  29770  elfix  29781  dffix2  29783  brcap  29818  funpartlem  29820  trer  30374  fneval  30410
  Copyright terms: Public domain W3C validator