Theorem brin 5163

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2147   ∩ cin 4092  ⟨cop 4840   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094  df-br 5109

This theorem is used by:  brinxp2  5737  trin2  6135  poirr2  6136  dfpo2  6325  predtrss  6351  tpostpos  8301  brinxper  8785  erinxp  8850  sbthcl  9156  infxpenlem  10131  fpwwe2lem11  10765  fpwwe2  10767  isinv  17985  isffth2  18143  ffthf1o  18146  ffthoppc  18151  ffthres2c  18167  isunit  20654  opsrtoslem2  22420  zsoring  28852  posrasymb  33624  trleile  33628  satefvfmla1  36398  brtxp  36857  idsset  36867  dfon3  36869  elfix  36880  dffix2  36882  brcap  36917  funpartlem  36921  trer  37319  fneval  37355  comodular  38207  brcnvin  39576  brxrn  39581  brin2  39636  br1cossinres  39735  grumnud  45531  chnrin  48179