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

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

Proof of Theorem brin
StepHypRef Expression
1 elin 3875 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5034 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 5034 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 5034 . . 3 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
53, 4anbi12i 630 . 2 ((𝐴𝑅𝐵𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
61, 2, 53bitr4i 307 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2112   ∩ cin 3858  ⟨cop 4529   class class class wbr 5033 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3866  df-br 5034 This theorem is referenced by:  brinxp2  5599  trin2  5956  poirr2  5957  tpostpos  7923  erinxp  8382  sbthcl  8661  infxpenlem  9466  fpwwe2lem11  10094  fpwwe2  10096  isinv  17082  isffth2  17238  ffthf1o  17241  ffthoppc  17246  ffthres2c  17262  isunit  19471  opsrtoslem2  20809  posrasymb  30759  trleile  30768  satefvfmla1  32896  dfpo2  33231  brtxp  33724  idsset  33734  dfon3  33736  elfix  33747  dffix2  33749  brcap  33784  funpartlem  33786  trer  34047  fneval  34083  brxrn  36059  brin2  36090  br1cossinres  36120  grumnud  41360
 Copyright terms: Public domain W3C validator