![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brin | Structured version Visualization version GIF version |
Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
Ref | Expression |
---|---|
brin | ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3960 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ∩ 𝑆) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 5142 | . 2 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑅 ∩ 𝑆)) | |
3 | df-br 5142 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
4 | df-br 5142 | . . 3 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
5 | 3, 4 | anbi12i 627 | . 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ 〈𝐴, 𝐵〉 ∈ 𝑆)) |
6 | 1, 2, 5 | 3bitr4i 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 |