Theorem relxp 5672

Description: A Cartesian 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 5670	. 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
2		df-rel 5661	. 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
3	1, 2	mpbir 231	1 ⊢ Rel (𝐴 × 𝐵)

Syntax hints:  Vcvv 3459   ⊆ wss 3926   × cxp 5652  Rel wrel 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  xpsspw  5788  relinxp  5793  inxp  5811  xpiindi  5815  eliunxp  5817  opeliunxp2  5818  relres  5992  restidsing  6040  codir  6109  qfto  6110  difxp  6153  sofld  6176  cnvcnv  6181  dfco2  6234  unixp  6271  ressn  6274  fliftcnv  7304  fliftfun  7305  oprssdm  7588  frxp  8125  frxp2  8143  frxp3  8150  opeliunxp2f  8209  reltpos  8230  tposfo  8252  tposf  8253  swoer  8750  xpider  8802  xpcomf1o  9075  fpwwe2lem8  10652  ordpinq  10957  addassnq  10972  mulassnq  10973  distrnq  10975  mulidnq  10977  recmulnq  10978  ltexnq  10989  prcdnq  11007  ltrel  11297  lerel  11299  dfle2  13163  fsumcom2  15790  fprodcom2  16000  0rest  17443  firest  17446  2oppchomf  17736  isinv  17773  invsym2  17776  invfun  17777  oppcsect2  17792  oppcinv  17793  oppchofcl  18272  oyoncl  18282  clatl  18518  gicer  19260  gsum2d2lem  19954  gsum2d2  19955  gsumcom2  19956  gsumxp  19957  dprd2d2  20027  mattpostpos  22392  mdetunilem9  22558  restbas  23096  txuni2  23503  txcls  23542  txdis1cn  23573  txkgen  23590  hmpher  23722  cnextrel  24001  tgphaus  24055  qustgplem  24059  tsmsxp  24093  utop2nei  24189  utop3cls  24190  xmeter  24372  caubl  25260  ovoliunlem1  25455  reldv  25823  taylf  26320  lgsquadlem1  27343  lgsquadlem2  27344  noseqrdgfn  28252  nvrel  30583  dfcnv2  32654  gsumpart  33051  gsumwrd2dccat  33061  elrgspnsubrunlem2  33243  qusxpid  33378  opprabs  33497  qtophaus  33867  cvmliftlem1  35307  cvmlift2lem12  35336  gonan0  35414  xpab  35743  dfso2  35772  relbigcup  35915  poimirlem3  37647  heicant  37679  vvdifopab  38278  cnvref4  38368  dvhopellsm  41136  dibvalrel  41182  dib1dim  41184  diclspsn  41213  dih1  41305  dih1dimatlem  41348  aoprssdm  47231  gricrel  47932  grlicrel  48011  eliunxp2  48309  iinxp  48809  coxp  48811  tposresxp  48858  tposf1o  48859  tposideq2  48864  joindm2  48942  meetdm2  48944  oppfvallem  49081  funcoppc3  49090  uptposlem  49130  reldmxpc  49163