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

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

Proof of Theorem brin
StepHypRef Expression
1 elin 3960 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5142 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 5142 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 5142 . . 3 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
53, 4anbi12i 627 . 2 ((𝐴𝑅𝐵𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
61, 2, 53bitr4i 302 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wcel 2106  cin 3943  cop 4628   class class class wbr 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-br 5142
This theorem is referenced by:  brinxp2  5745  trin2  6113  poirr2  6114  dfpo2  6284  predtrss  6312  tpostpos  8213  erinxp  8768  sbthcl  9078  infxpenlem  9990  fpwwe2lem11  10618  fpwwe2  10620  isinv  17689  isffth2  17849  ffthf1o  17852  ffthoppc  17857  ffthres2c  17873  isunit  20139  opsrtoslem2  21545  posrasymb  32006  trleile  32012  satefvfmla1  34245  brtxp  34680  idsset  34690  dfon3  34692  elfix  34703  dffix2  34705  brcap  34740  funpartlem  34742  trer  35003  fneval  35039  brcnvin  37043  brxrn  37047  brin2  37082  br1cossinres  37120  grumnud  42814
  Copyright terms: Public domain W3C validator