Theorem relxp 5641

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

Syntax hints:  Vcvv 3438   ⊆ wss 3905   × cxp 5621  Rel wrel 5628

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-opab 5158  df-xp 5629  df-rel 5630

This theorem is referenced by:  xpsspw  5756  relinxp  5761  inxp  5778  xpiindi  5782  eliunxp  5784  opeliunxp2  5785  relres  5960  restidsing  6008  codir  6073  qfto  6074  difxp  6117  sofld  6140  cnvcnv  6145  dfco2  6198  unixp  6234  ressn  6237  fliftcnv  7252  fliftfun  7253  oprssdm  7534  frxp  8066  frxp2  8084  frxp3  8091  opeliunxp2f  8150  reltpos  8171  tposfo  8193  tposf  8194  swoer  8663  xpider  8722  xpcomf1o  8990  fpwwe2lem8  10551  ordpinq  10856  addassnq  10871  mulassnq  10872  distrnq  10874  mulidnq  10876  recmulnq  10877  ltexnq  10888  prcdnq  10906  ltrel  11196  lerel  11198  dfle2  13067  fsumcom2  15699  fprodcom2  15909  0rest  17351  firest  17354  2oppchomf  17648  isinv  17685  invsym2  17688  invfun  17689  oppcsect2  17704  oppcinv  17705  oppchofcl  18184  oyoncl  18194  clatl  18432  gicer  19174  gsum2d2lem  19870  gsum2d2  19871  gsumcom2  19872  gsumxp  19873  dprd2d2  19943  mattpostpos  22357  mdetunilem9  22523  restbas  23061  txuni2  23468  txcls  23507  txdis1cn  23538  txkgen  23555  hmpher  23687  cnextrel  23966  tgphaus  24020  qustgplem  24024  tsmsxp  24058  utop2nei  24154  utop3cls  24155  xmeter  24337  caubl  25224  ovoliunlem1  25419  reldv  25787  taylf  26284  lgsquadlem1  27307  lgsquadlem2  27308  noseqrdgfn  28223  nvrel  30564  dfcnv2  32633  gsumpart  33023  gsumwrd2dccat  33033  elrgspnsubrunlem2  33201  qusxpid  33313  opprabs  33432  qtophaus  33805  cvmliftlem1  35260  cvmlift2lem12  35289  gonan0  35367  xpab  35701  dfso2  35730  relbigcup  35873  poimirlem3  37605  heicant  37637  vvdifopab  38237  cnvref4  38320  dvhopellsm  41099  dibvalrel  41145  dib1dim  41147  diclspsn  41176  dih1  41268  dih1dimatlem  41311  aoprssdm  47190  gricrel  47907  grlicrel  47994  eliunxp2  48322  iinxp  48819  coxp  48821  xpco2  48845  tposresxp  48871  tposf1o  48872  tposideq2  48877  joindm2  48956  meetdm2  48958  oppfvallem  49124  funcoppc3  49136  uptposlem  49186  reldmxpc  49235