Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > relxp | Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpss 4446 | . 2 | |
2 | df-rel 4352 | . 2 | |
3 | 1, 2 | mpbir 134 | 1 |
Colors of variables: wff set class |
Syntax hints: cvv 2557 wss 2917 cxp 4343 wrel 4350 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-v 2559 df-in 2924 df-ss 2931 df-opab 3819 df-xp 4351 df-rel 4352 |
This theorem is referenced by: xpiindim 4473 eliunxp 4475 opeliunxp2 4476 relres 4639 codir 4713 qfto 4714 cnvcnv 4773 dfco2 4820 unixpm 4853 ressn 4858 fliftcnv 5435 fliftfun 5436 reltpos 5865 tpostpos 5879 tposfo 5886 tposf 5887 swoer 6134 xpiderm 6177 erinxp 6180 xpcomf1o 6299 ltrel 7081 lerel 7083 |
Copyright terms: Public domain | W3C validator |