Theorem relxp 4884

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 4883	. 2 |- ( A X. B ) C_ ( _V X. _V )
2		df-rel 4781	. 2 |- ( Rel ( A X. B ) <-> ( A X. B ) C_ ( _V X. _V ) )
3	1, 2	mpbir 146	1 |- Rel ( A X. B )

This proof depends on syntax axioms:   _Vcvv 2821   C_ wss 3220   X. cxp 4772   Rel wrel 4779

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233  df-opab 4193  df-xp 4780  df-rel 4781

This theorem is used by:  xpiindim  4917  eliunxp  4919  opeliunxp2  4920  relres  5091  restidsing  5119  codir  5176  qfto  5177  cnvcnv  5240  dfco2  5287  unixpm  5323  ressn  5328  fliftcnv  6001  fliftfun  6002  opeliunxp2f  6509  reltpos  6521  tpostpos  6535  tposfo  6542  tposf  6543  swoer  6835  xpider  6880  erinxp  6883  xpcomf1o  7123  ltrel  8387  lerel  8389  fisumcom2  12205  fprodcom2fi  12393  txuni2  15357  txdis1cn  15379  xmeter  15537  reldvg  15780  lgsquadlem1  16196  lgsquadlem2  16197