Theorem relxp 4735

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 4734	. 2 |- ( A X. B ) C_ ( _V X. _V )
2		df-rel 4633	. 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 2737   C_ wss 3129   X. cxp 4624   Rel wrel 4631

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-in 3135  df-ss 3142  df-opab 4065  df-xp 4632  df-rel 4633

This theorem is referenced by:  xpiindim  4764  eliunxp  4766  opeliunxp2  4767  relres  4935  restidsing  4963  codir  5017  qfto  5018  cnvcnv  5081  dfco2  5128  unixpm  5164  ressn  5169  fliftcnv  5795  fliftfun  5796  opeliunxp2f  6238  reltpos  6250  tpostpos  6264  tposfo  6271  tposf  6272  swoer  6562  xpider  6605  erinxp  6608  xpcomf1o  6824  ltrel  8018  lerel  8020  fisumcom2  11445  fprodcom2fi  11633  txuni2  13726  txdis1cn  13748  xmeter  13906  reldvg  14118