Theorem relxp 5607

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

Syntax hints:  Vcvv 3432   ⊆ wss 3887   × cxp 5587  Rel wrel 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596

This theorem is referenced by:  xpsspw  5719  relinxp  5724  xpiindi  5744  eliunxp  5746  opeliunxp2  5747  relres  5920  restidsing  5962  codir  6025  qfto  6026  difxp  6067  sofld  6090  cnvcnv  6095  dfco2  6149  unixp  6185  ressn  6188  fliftcnv  7182  fliftfun  7183  oprssdm  7453  frxp  7967  opeliunxp2f  8026  reltpos  8047  tposfo  8069  tposf  8070  swoer  8528  xpider  8577  xpcomf1o  8848  fpwwe2lem8  10394  ordpinq  10699  addassnq  10714  mulassnq  10715  distrnq  10717  mulidnq  10719  recmulnq  10720  ltexnq  10731  prcdnq  10749  ltrel  11037  lerel  11039  dfle2  12881  fsumcom2  15486  fprodcom2  15694  0rest  17140  firest  17143  2oppchomf  17435  isinv  17472  invsym2  17475  invfun  17476  oppcsect2  17491  oppcinv  17492  oppchofcl  17978  oyoncl  17988  clatl  18226  gicer  18892  gsum2d2lem  19574  gsum2d2  19575  gsumcom2  19576  gsumxp  19577  dprd2d2  19647  mattpostpos  21603  mdetunilem9  21769  restbas  22309  txuni2  22716  txcls  22755  txdis1cn  22786  txkgen  22803  hmpher  22935  cnextrel  23214  tgphaus  23268  qustgplem  23272  tsmsxp  23306  utop2nei  23402  utop3cls  23403  xmeter  23586  caubl  24472  ovoliunlem1  24666  reldv  25034  taylf  25520  lgsquadlem1  26528  lgsquadlem2  26529  nvrel  28964  dfcnv2  31013  gsumpart  31315  qusxpid  31559  qtophaus  31786  cvmliftlem1  33247  cvmlift2lem12  33276  gonan0  33354  xpab  33677  dfso2  33722  frxp2  33791  frxp3  33797  relbigcup  34199  poimirlem3  35780  heicant  35812  vvdifopab  36399  dvhopellsm  39131  dibvalrel  39177  dib1dim  39179  diclspsn  39208  dih1  39300  dih1dimatlem  39343  aoprssdm  44694  eliunxp2  45669  joindm2  46262  meetdm2  46264