Theorem relxp 4784

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

Step	Hyp	Ref	Expression
1		xpss 4783	. 2 |- ( A X. B ) C_ ( _V X. _V )
2		df-rel 4682	. 2 |- ( Rel ( A X. B ) <-> ( A X. B ) C_ ( _V X. _V ) )
3	1, 2	mpbir 146	1 |- Rel ( A X. B )

Syntax hints:   _Vcvv 2772   C_ wss 3166   X. cxp 4673   Rel wrel 4680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179  df-opab 4106  df-xp 4681  df-rel 4682

This theorem is referenced by:  xpiindim  4815  eliunxp  4817  opeliunxp2  4818  relres  4987  restidsing  5015  codir  5071  qfto  5072  cnvcnv  5135  dfco2  5182  unixpm  5218  ressn  5223  fliftcnv  5864  fliftfun  5865  opeliunxp2f  6324  reltpos  6336  tpostpos  6350  tposfo  6357  tposf  6358  swoer  6648  xpider  6693  erinxp  6696  xpcomf1o  6920  ltrel  8134  lerel  8136  fisumcom2  11749  fprodcom2fi  11937  txuni2  14728  txdis1cn  14750  xmeter  14908  reldvg  15151  lgsquadlem1  15554  lgsquadlem2  15555