Theorem relxp 4465

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 4464	. 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
2		df-rel 4370	. 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
3	1, 2	mpbir 144	1 ⊢ Rel (𝐴 × 𝐵)

Syntax hints:  Vcvv 2601   ⊆ wss 2973   × cxp 4361  Rel wrel 4368

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-in 2979  df-ss 2986  df-opab 3840  df-xp 4369  df-rel 4370

This theorem is referenced by:  xpiindim  4491  eliunxp  4493  opeliunxp2  4494  relres  4657  codir  4733  qfto  4734  cnvcnv  4793  dfco2  4840  unixpm  4873  ressn  4878  fliftcnv  5455  fliftfun  5456  reltpos  5888  tpostpos  5902  tposfo  5909  tposf  5910  swoer  6157  xpiderm  6200  erinxp  6203  xpcomf1o  6322  ltrel  7174  lerel  7176