Theorem relxp 5703

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

Syntax hints:  Vcvv 3480   ⊆ wss 3951   × cxp 5683  Rel wrel 5690

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  xpsspw  5819  relinxp  5824  inxp  5842  xpiindi  5846  eliunxp  5848  opeliunxp2  5849  relres  6023  restidsing  6071  codir  6140  qfto  6141  difxp  6184  sofld  6207  cnvcnv  6212  dfco2  6265  unixp  6302  ressn  6305  fliftcnv  7331  fliftfun  7332  oprssdm  7614  frxp  8151  frxp2  8169  frxp3  8176  opeliunxp2f  8235  reltpos  8256  tposfo  8278  tposf  8279  swoer  8776  xpider  8828  xpcomf1o  9101  fpwwe2lem8  10678  ordpinq  10983  addassnq  10998  mulassnq  10999  distrnq  11001  mulidnq  11003  recmulnq  11004  ltexnq  11015  prcdnq  11033  ltrel  11323  lerel  11325  dfle2  13189  fsumcom2  15810  fprodcom2  16020  0rest  17474  firest  17477  2oppchomf  17767  isinv  17804  invsym2  17807  invfun  17808  oppcsect2  17823  oppcinv  17824  oppchofcl  18305  oyoncl  18315  clatl  18553  gicer  19295  gsum2d2lem  19991  gsum2d2  19992  gsumcom2  19993  gsumxp  19994  dprd2d2  20064  mattpostpos  22460  mdetunilem9  22626  restbas  23166  txuni2  23573  txcls  23612  txdis1cn  23643  txkgen  23660  hmpher  23792  cnextrel  24071  tgphaus  24125  qustgplem  24129  tsmsxp  24163  utop2nei  24259  utop3cls  24260  xmeter  24443  caubl  25342  ovoliunlem1  25537  reldv  25905  taylf  26402  lgsquadlem1  27424  lgsquadlem2  27425  noseqrdgfn  28312  nvrel  30621  dfcnv2  32686  gsumpart  33060  gsumwrd2dccat  33070  elrgspnsubrunlem2  33252  qusxpid  33391  opprabs  33510  qtophaus  33835  cvmliftlem1  35290  cvmlift2lem12  35319  gonan0  35397  xpab  35726  dfso2  35755  relbigcup  35898  poimirlem3  37630  heicant  37662  vvdifopab  38261  cnvref4  38351  dvhopellsm  41119  dibvalrel  41165  dib1dim  41167  diclspsn  41196  dih1  41288  dih1dimatlem  41331  aoprssdm  47214  gricrel  47888  grlicrel  47966  eliunxp2  48250  coxp  48744  tposresxp  48783  tposf1o  48784  tposideq2  48789  joindm2  48865  meetdm2  48867  reldmxpc  48952