![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relinxp | Structured version Visualization version GIF version |
Description: Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019.) |
Ref | Expression |
---|---|
relinxp | ⊢ Rel (𝑅 ∩ (𝐴 × 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relxp 5692 | . 2 ⊢ Rel (𝐴 × 𝐵) | |
2 | relin2 5811 | . 2 ⊢ (Rel (𝐴 × 𝐵) → Rel (𝑅 ∩ (𝐴 × 𝐵))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Rel (𝑅 ∩ (𝐴 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ∩ cin 3945 × cxp 5672 Rel wrel 5679 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-in 3953 df-ss 3963 df-opab 5208 df-xp 5680 df-rel 5681 |
This theorem is referenced by: inxp 5830 elinxp 6020 cnvcnv 6195 tpostpos 8253 brinxper 8755 erinxp 8812 brdom3 10562 brdom5 10563 brdom4 10564 fpwwe2lem7 10671 fpwwe2lem8 10672 fpwwe2lem11 10675 pwsle 17502 opsrtoslem2 22065 elrn3 35597 bj-idres 36880 br1cnvinxp 37967 inxprnres 38003 inxpss 38022 inxpss2 38026 iss2 38055 inxp2 38078 inxpxrn 38106 gricer 47508 |
Copyright terms: Public domain | W3C validator |