Theorem brin 4704

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

Step	Hyp	Ref	Expression
1		elin 3796	. 2 |- ( <. A , B >. e. ( R i^i S ) <-> ( <. A , B >. e. R /\ <. A , B >. e. S ) )
2		df-br 4654	. 2 |- ( A ( R i^i S ) B <-> <. A , B >. e. ( R i^i S ) )
3		df-br 4654	. . 3 |- ( A R B <-> <. A , B >. e. R )
4		df-br 4654	. . 3 |- ( A S B <-> <. A , B >. e. S )
5	3, 4	anbi12i 733	. 2 |- ( ( A R B /\ A S B ) <-> ( <. A , B >. e. R /\ <. A , B >. e. S ) )
6	1, 2, 5	3bitr4i 292	1 |- ( A ( R i^i S ) B <-> ( A R B /\ A S B ) )

Syntax hints:   <-> wb 196   /\ wa 384   e. wcel 1990   i^i cin 3573   <.cop 4183   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-br 4654

This theorem is referenced by:  brinxp2  5180  trin2  5519  poirr2  5520  tpostpos  7372  erinxp  7821  sbthcl  8082  infxpenlem  8836  fpwwe2lem12  9463  fpwwe2  9465  isinv  16420  isffth2  16576  ffthf1o  16579  ffthoppc  16584  ffthres2c  16600  isunit  18657  opsrtoslem2  19485  posrasymb  29657  trleile  29666  dfpo2  31645  brtxp  31987  idsset  31997  dfon3  31999  elfix  32010  dffix2  32012  brcap  32047  funpartlem  32049  trer  32310  fneval  32347  brinxp2ALTV  34034