Theorem brin 5195

Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008.)

Assertion

Ref	Expression
brin	⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))

Proof of Theorem brin

Step	Hyp	Ref	Expression
1		elin 3967	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5144	. 2 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆))
3		df-br 5144	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5144	. . 3 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	3, 4	anbi12i 628	. 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
6	1, 2, 5	3bitr4i 303	1 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   ∩ cin 3950  ⟨cop 4632   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-br 5144

This theorem is referenced by:  brinxp2  5763  trin2  6143  poirr2  6144  dfpo2  6316  predtrss  6343  tpostpos  8271  brinxper  8774  erinxp  8831  sbthcl  9135  infxpenlem  10053  fpwwe2lem11  10681  fpwwe2  10683  isinv  17804  isffth2  17963  ffthf1o  17966  ffthoppc  17971  ffthres2c  17987  isunit  20373  opsrtoslem2  22080  posrasymb  32955  trleile  32961  satefvfmla1  35430  brtxp  35881  idsset  35891  dfon3  35893  elfix  35904  dffix2  35906  brcap  35941  funpartlem  35943  trer  36317  fneval  36353  brcnvin  38371  brxrn  38375  brin2  38410  br1cossinres  38448  grumnud  44305