Theorem relxp 4858

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 (𝐴 × 𝐵)

Proof of Theorem relxp

Step	Hyp	Ref	Expression
1		xpss 4857	. 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
2		df-rel 4755	. 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
3	1, 2	mpbir 146	1 ⊢ Rel (𝐴 × 𝐵)

Syntax hints:  Vcvv 2812   ⊆ wss 3210   × cxp 4746  Rel wrel 4753

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-in 3216  df-ss 3223  df-opab 4171  df-xp 4754  df-rel 4755

This theorem is referenced by:  xpiindim  4891  eliunxp  4893  opeliunxp2  4894  relres  5065  restidsing  5093  codir  5150  qfto  5151  cnvcnv  5214  dfco2  5261  unixpm  5297  ressn  5302  fliftcnv  5967  fliftfun  5968  opeliunxp2f  6468  reltpos  6480  tpostpos  6494  tposfo  6501  tposf  6502  swoer  6794  xpider  6839  erinxp  6842  xpcomf1o  7075  ltrel  8334  lerel  8336  fisumcom2  12120  fprodcom2fi  12308  txuni2  15113  txdis1cn  15135  xmeter  15293  reldvg  15536  lgsquadlem1  15942  lgsquadlem2  15943