Theorem relxp 5642

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

Syntax hints:  Vcvv 3430   ⊆ wss 3890   × cxp 5622  Rel wrel 5629

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-opab 5149  df-xp 5630  df-rel 5631

This theorem is referenced by:  xpsspw  5758  relinxp  5763  inxp  5780  xpiindi  5784  eliunxp  5786  opeliunxp2  5787  relres  5964  restidsing  6012  codir  6077  qfto  6078  difxp  6122  sofld  6145  cnvcnv  6150  dfco2  6203  unixp  6240  ressn  6243  fliftcnv  7259  fliftfun  7260  oprssdm  7541  frxp  8069  frxp2  8087  frxp3  8094  opeliunxp2f  8153  reltpos  8174  tposfo  8196  tposf  8197  swoer  8668  xpider  8728  xpcomf1o  8997  fpwwe2lem8  10552  ordpinq  10857  addassnq  10872  mulassnq  10873  distrnq  10875  mulidnq  10877  recmulnq  10878  ltexnq  10889  prcdnq  10907  ltrel  11198  lerel  11200  dfle2  13089  fsumcom2  15727  fprodcom2  15940  0rest  17383  firest  17386  2oppchomf  17681  isinv  17718  invsym2  17721  invfun  17722  oppcsect2  17737  oppcinv  17738  oppchofcl  18217  oyoncl  18227  clatl  18465  gicer  19243  gsum2d2lem  19939  gsum2d2  19940  gsumcom2  19941  gsumxp  19942  dprd2d2  20012  mattpostpos  22429  mdetunilem9  22595  restbas  23133  txuni2  23540  txcls  23579  txdis1cn  23610  txkgen  23627  hmpher  23759  cnextrel  24038  tgphaus  24092  qustgplem  24096  tsmsxp  24130  utop2nei  24225  utop3cls  24226  xmeter  24408  caubl  25285  ovoliunlem1  25479  reldv  25847  taylf  26337  lgsquadlem1  27357  lgsquadlem2  27358  noseqrdgfn  28312  nvrel  30688  dfcnv2  32763  gsumpart  33139  gsumwrd2dccat  33154  elrgspnsubrunlem2  33324  qusxpid  33438  opprabs  33557  qtophaus  33996  cvmliftlem1  35483  cvmlift2lem12  35512  gonan0  35590  xpab  35924  dfso2  35953  relbigcup  36093  poimirlem3  37958  heicant  37990  vvdifopab  38600  cnvref4  38685  ecxrn2  38743  dvhopellsm  41577  dibvalrel  41623  dib1dim  41625  diclspsn  41654  dih1  41746  dih1dimatlem  41789  aoprssdm  47662  gricrel  48407  grlicrel  48494  eliunxp2  48822  iinxp  49318  coxp  49320  xpco2  49344  tposresxp  49370  tposf1o  49371  tposideq2  49376  joindm2  49455  meetdm2  49457  oppfvallem  49622  funcoppc3  49634  uptposlem  49684  reldmxpc  49733