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

Theorem relxp 4606
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  ( A  X.  B )

Proof of Theorem relxp
StepHypRef Expression
1 xpss 4605 . 2  |-  ( A  X.  B )  C_  ( _V  X.  _V )
2 df-rel 4504 . 2  |-  ( Rel  ( A  X.  B
)  <->  ( A  X.  B )  C_  ( _V  X.  _V ) )
31, 2mpbir 145 1  |-  Rel  ( A  X.  B )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2655    C_ wss 3035    X. cxp 4495   Rel wrel 4502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-in 3041  df-ss 3048  df-opab 3948  df-xp 4503  df-rel 4504
This theorem is referenced by:  xpiindim  4634  eliunxp  4636  opeliunxp2  4637  relres  4803  codir  4883  qfto  4884  cnvcnv  4947  dfco2  4994  unixpm  5030  ressn  5035  fliftcnv  5648  fliftfun  5649  opeliunxp2f  6087  reltpos  6099  tpostpos  6113  tposfo  6120  tposf  6121  swoer  6409  xpider  6452  erinxp  6455  xpcomf1o  6670  ltrel  7744  lerel  7746  fisumcom2  11093  txuni2  12261  txdis1cn  12283  xmeter  12419  reldvg  12597
  Copyright terms: Public domain W3C validator