Theorem brin 5156

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 4092	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5103	. 2 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∩ 𝑆))
3		df-br 5103	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5103	. . 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 2144   ∩ cin 4088  ⟨cop 4834   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090  df-br 5103

This theorem is used by:  brinxp2  5730  trin2  6119  poirr2  6120  dfpo2  6302  predtrss  6328  tpostpos  8270  brinxper  8754  erinxp  8819  sbthcl  9125  infxpenlem  10099  fpwwe2lem11  10733  fpwwe2  10735  isinv  17944  isffth2  18102  ffthf1o  18105  ffthoppc  18110  ffthres2c  18126  isunit  20612  opsrtoslem2  22374  zsoring  28804  posrasymb  33578  trleile  33582  satefvfmla1  36280  brtxp  36738  idsset  36748  dfon3  36750  elfix  36761  dffix2  36763  brcap  36798  funpartlem  36802  trer  37200  fneval  37236  brcnvin  39419  brxrn  39424  brin2  39479  br1cossinres  39578  grumnud  45379  chnrin  48014