Theorem relxp 5537

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

Syntax hints:  Vcvv 3441   ⊆ wss 3881   × cxp 5517  Rel wrel 5524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-opab 5093  df-xp 5525  df-rel 5526

This theorem is referenced by:  xpsspw  5646  relinxp  5651  xpiindi  5670  eliunxp  5672  opeliunxp2  5673  relres  5847  restidsing  5889  codir  5947  qfto  5948  difxp  5988  sofld  6011  cnvcnv  6016  dfco2  6065  unixp  6101  ressn  6104  fliftcnv  7043  fliftfun  7044  oprssdm  7309  frxp  7803  opeliunxp2f  7859  reltpos  7880  tposfo  7902  tposf  7903  swoer  8302  xpider  8351  xpcomf1o  8589  fpwwe2lem9  10049  ordpinq  10354  addassnq  10369  mulassnq  10370  distrnq  10372  mulidnq  10374  recmulnq  10375  ltexnq  10386  prcdnq  10404  ltrel  10692  lerel  10694  dfle2  12528  fsumcom2  15121  fprodcom2  15330  0rest  16695  firest  16698  2oppchomf  16986  isinv  17022  invsym2  17025  invfun  17026  oppcsect2  17041  oppcinv  17042  oppchofcl  17502  oyoncl  17512  clatl  17718  gicer  18408  gsum2d2lem  19086  gsum2d2  19087  gsumcom2  19088  gsumxp  19089  dprd2d2  19159  mattpostpos  21059  mdetunilem9  21225  restbas  21763  txuni2  22170  txcls  22209  txdis1cn  22240  txkgen  22257  hmpher  22389  cnextrel  22668  tgphaus  22722  qustgplem  22726  tsmsxp  22760  utop2nei  22856  utop3cls  22857  xmeter  23040  caubl  23912  ovoliunlem1  24106  reldv  24473  taylf  24956  lgsquadlem1  25964  lgsquadlem2  25965  nvrel  28385  dfcnv2  30439  gsumpart  30740  qusxpid  30979  qtophaus  31189  cvmliftlem1  32645  cvmlift2lem12  32674  gonan0  32752  dfso2  33103  relbigcup  33471  poimirlem3  35060  heicant  35092  vvdifopab  35681  dvhopellsm  38413  dibvalrel  38459  dib1dim  38461  diclspsn  38490  dih1  38582  dih1dimatlem  38625  aoprssdm  43758  eliunxp2  44735