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

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

Proof of Theorem brin
StepHypRef Expression
1 elin 3979 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5149 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 5149 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 5149 . . 3 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
53, 4anbi12i 628 . 2 ((𝐴𝑅𝐵𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
61, 2, 53bitr4i 303 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wcel 2106  cin 3962  cop 4637   class class class wbr 5148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-br 5149
This theorem is referenced by:  brinxp2  5766  trin2  6146  poirr2  6147  dfpo2  6318  predtrss  6345  tpostpos  8270  brinxper  8773  erinxp  8830  sbthcl  9134  infxpenlem  10051  fpwwe2lem11  10679  fpwwe2  10681  isinv  17808  isffth2  17970  ffthf1o  17973  ffthoppc  17978  ffthres2c  17994  isunit  20390  opsrtoslem2  22098  posrasymb  32940  trleile  32946  satefvfmla1  35410  brtxp  35862  idsset  35872  dfon3  35874  elfix  35885  dffix2  35887  brcap  35922  funpartlem  35924  trer  36299  fneval  36335  brcnvin  38352  brxrn  38356  brin2  38391  br1cossinres  38429  grumnud  44282
  Copyright terms: Public domain W3C validator