ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  relxp GIF version

Theorem relxp 4708
Description: A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
relxp Rel (𝐴 × 𝐵)

Proof of Theorem relxp
StepHypRef Expression
1 xpss 4707 . 2 (𝐴 × 𝐵) ⊆ (V × V)
2 df-rel 4606 . 2 (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
31, 2mpbir 145 1 Rel (𝐴 × 𝐵)
Colors of variables: wff set class
Syntax hints:  Vcvv 2722  wss 3112   × cxp 4597  Rel wrel 4604
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2724  df-in 3118  df-ss 3125  df-opab 4039  df-xp 4605  df-rel 4606
This theorem is referenced by:  xpiindim  4736  eliunxp  4738  opeliunxp2  4739  relres  4907  codir  4987  qfto  4988  cnvcnv  5051  dfco2  5098  unixpm  5134  ressn  5139  fliftcnv  5758  fliftfun  5759  opeliunxp2f  6198  reltpos  6210  tpostpos  6224  tposfo  6231  tposf  6232  swoer  6521  xpider  6564  erinxp  6567  xpcomf1o  6783  ltrel  7952  lerel  7954  fisumcom2  11369  fprodcom2fi  11557  txuni2  12823  txdis1cn  12845  xmeter  13003  reldvg  13215
  Copyright terms: Public domain W3C validator