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

Theorem brin 5195
Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
Assertion
Ref Expression
brin (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))

Proof of Theorem brin
StepHypRef Expression
1 elin 3967 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5144 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 5144 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 5144 . . 3 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
53, 4anbi12i 628 . 2 ((𝐴𝑅𝐵𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
61, 2, 53bitr4i 303 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator