Theorem relxp 5669

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

Syntax hints:  Vcvv 3457   ⊆ wss 3907   × cxp 5649  Rel wrel 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-opab 5167  df-xp 5657  df-rel 5658

This theorem is referenced by:  xpsspw  5786  relinxp  5791  inxp  5808  xpiindi  5811  eliunxp  5813  opeliunxp2  5814  relres  5994  restidsing  6045  codir  6110  qfto  6111  difxp  6152  sofld  6176  cnvcnv  6181  dfco2  6235  unixp  6272  ressn  6275  fliftcnv  7299  fliftfun  7300  oprssdm  7581  frxp  8110  frxp2  8128  frxp3  8135  opeliunxp2f  8194  reltpos  8215  tposfo  8237  tposf  8238  swoer  8714  xpider  8774  xpcomf1o  9042  fpwwe2lem8  10611  ordpinq  10916  addassnq  10931  mulassnq  10932  distrnq  10934  mulidnq  10936  recmulnq  10937  ltexnq  10948  prcdnq  10966  ltrel  11259  lerel  11261  dfle2  13160  fsumcom2  15813  fprodcom2  16026  0rest  17470  firest  17473  2oppchomf  17768  isinv  17805  invsym2  17808  invfun  17809  oppcsect2  17824  oppcinv  17825  oppchofcl  18304  oyoncl  18314  clatl  18552  qusxpid  19239  gicer  19335  gsum2d2lem  20031  gsum2d2  20032  gsumcom2  20033  gsumxp  20034  dprd2d2  20104  mattpostpos  22568  mdetunilem9  22734  restbas  23272  txuni2  23679  txcls  23718  txdis1cn  23749  txkgen  23766  hmpher  23898  cnextrel  24177  tgphaus  24231  qustgplem  24235  tsmsxp  24269  utop2nei  24364  utop3cls  24365  xmeter  24547  caubl  25424  ovoliunlem1  25618  reldv  25986  taylf  26478  lgsquadlem1  27498  lgsquadlem2  27499  noseqrdgfn  28453  nvrel  30859  dfcnv2  32928  gsumpart  33291  gsumwrd2dccat  33306  elrgspnsubrunlem2  33476  opprabs  33676  qtophaus  34138  cvmliftlem1  35643  cvmlift2lem12  35672  gonan0  35750  xpab  36084  dfso2  36113  relbigcup  36253  poimirlem3  38129  heicant  38161  vvdifopab  38771  cnvref4  38856  ecxrn2  38914  dvhopellsm  41748  dibvalrel  41794  dib1dim  41796  diclspsn  41825  dih1  41917  dih1dimatlem  41960  aoprssdm  47795  gricrel  48540  grlicrel  48627  eliunxp2  48966  iinxp  49461  coxp  49463  xpco2  49487  tposresxp  49513  tposf1o  49514  tposideq2  49519  joindm2  49598  meetdm2  49600  oppfvallem  49765  funcoppc3  49777  uptposlem  49827  reldmxpc  49876