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 4168 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ∩ 𝑆) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 5066 | . 2 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑅 ∩ 𝑆)) | |
3 | df-br 5066 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
4 | df-br 5066 | . . 3 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
5 | 3, 4 | anbi12i 628 | . 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∧ 〈𝐴, 𝐵〉 ∈ 𝑆)) |
6 | 1, 2, 5 | 3bitr4i 305 | 1 ⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∈ wcel 2110 ∩ cin 3934 〈cop 4572 class class class wbr 5065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-in 3942 df-br 5066 |
This theorem is referenced by: brinxp2 5628 trin2 5982 poirr2 5983 tpostpos 7911 erinxp 8370 sbthcl 8638 infxpenlem 9438 fpwwe2lem12 10062 fpwwe2 10064 isinv 17029 isffth2 17185 ffthf1o 17188 ffthoppc 17193 ffthres2c 17209 isunit 19406 opsrtoslem2 20264 posrasymb 30644 trleile 30653 satefvfmla1 32672 dfpo2 32991 brtxp 33341 idsset 33351 dfon3 33353 elfix 33364 dffix2 33366 brcap 33401 funpartlem 33403 trer 33664 fneval 33700 brxrn 35625 brin2 35656 br1cossinres 35686 grumnud 40620 |
Copyright terms: Public domain | W3C validator |