Theorem brin 5152

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 3920	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5101	. 2 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆))
3		df-br 5101	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5101	. . 3 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	3, 4	anbi12i 637	. 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
6	1, 2, 5	3bitr4i 305	1 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2142   ∩ cin 3903  ⟨cop 4588   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-br 5101

This theorem is referenced by:  brinxp2  5725  trin2  6110  poirr2  6111  dfpo2  6283  predtrss  6309  tpostpos  8226  brinxper  8708  erinxp  8773  sbthcl  9071  infxpenlem  9969  fpwwe2lem11  10599  fpwwe2  10601  isinv  17793  isffth2  17951  ffthf1o  17954  ffthoppc  17959  ffthres2c  17975  isunit  20418  opsrtoslem2  22106  zsoring  28499  posrasymb  33142  trleile  33146  satefvfmla1  35772  brtxp  36225  idsset  36235  dfon3  36237  elfix  36248  dffix2  36250  brcap  36285  funpartlem  36289  trer  36673  fneval  36709  brcnvin  38874  brxrn  38879  brin2  38934  br1cossinres  39033  grumnud  44859