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

Step	Hyp	Ref	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 ) )
3	1, 2	mpbir 145	1 |- Rel ( A X. B )

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