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

Theorem relxp 4618
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 4617 . 2 (𝐴 × 𝐵) ⊆ (V × V)
2 df-rel 4516 . 2 (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
31, 2mpbir 145 1 Rel (𝐴 × 𝐵)
Colors of variables: wff set class
Syntax hints:  Vcvv 2660  wss 3041   × cxp 4507  Rel wrel 4514
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-in 3047  df-ss 3054  df-opab 3960  df-xp 4515  df-rel 4516
This theorem is referenced by:  xpiindim  4646  eliunxp  4648  opeliunxp2  4649  relres  4817  codir  4897  qfto  4898  cnvcnv  4961  dfco2  5008  unixpm  5044  ressn  5049  fliftcnv  5664  fliftfun  5665  opeliunxp2f  6103  reltpos  6115  tpostpos  6129  tposfo  6136  tposf  6137  swoer  6425  xpider  6468  erinxp  6471  xpcomf1o  6687  ltrel  7794  lerel  7796  fisumcom2  11162  txuni2  12336  txdis1cn  12358  xmeter  12516  reldvg  12728
  Copyright terms: Public domain W3C validator