![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > relxp | GIF version |
Description: A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
relxp | ⊢ Rel (𝐴 × 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpss 4655 | . 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V) | |
2 | df-rel 4554 | . 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V)) | |
3 | 1, 2 | mpbir 145 | 1 ⊢ Rel (𝐴 × 𝐵) |
Colors of variables: wff set class |
Syntax hints: Vcvv 2689 ⊆ wss 3076 × cxp 4545 Rel wrel 4552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-in 3082 df-ss 3089 df-opab 3998 df-xp 4553 df-rel 4554 |
This theorem is referenced by: xpiindim 4684 eliunxp 4686 opeliunxp2 4687 relres 4855 codir 4935 qfto 4936 cnvcnv 4999 dfco2 5046 unixpm 5082 ressn 5087 fliftcnv 5704 fliftfun 5705 opeliunxp2f 6143 reltpos 6155 tpostpos 6169 tposfo 6176 tposf 6177 swoer 6465 xpider 6508 erinxp 6511 xpcomf1o 6727 ltrel 7850 lerel 7852 fisumcom2 11239 txuni2 12464 txdis1cn 12486 xmeter 12644 reldvg 12856 |
Copyright terms: Public domain | W3C validator |