Theorem relxp 5649

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

Syntax hints:  Vcvv 3429   ⊆ wss 3889   × cxp 5629  Rel wrel 5636

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  xpsspw  5765  relinxp  5770  inxp  5787  xpiindi  5790  eliunxp  5792  opeliunxp2  5793  relres  5970  restidsing  6018  codir  6083  qfto  6084  difxp  6128  sofld  6151  cnvcnv  6156  dfco2  6209  unixp  6246  ressn  6249  fliftcnv  7266  fliftfun  7267  oprssdm  7548  frxp  8076  frxp2  8094  frxp3  8101  opeliunxp2f  8160  reltpos  8181  tposfo  8203  tposf  8204  swoer  8675  xpider  8735  xpcomf1o  9004  fpwwe2lem8  10561  ordpinq  10866  addassnq  10881  mulassnq  10882  distrnq  10884  mulidnq  10886  recmulnq  10887  ltexnq  10898  prcdnq  10916  ltrel  11207  lerel  11209  dfle2  13098  fsumcom2  15736  fprodcom2  15949  0rest  17392  firest  17395  2oppchomf  17690  isinv  17727  invsym2  17730  invfun  17731  oppcsect2  17746  oppcinv  17747  oppchofcl  18226  oyoncl  18236  clatl  18474  gicer  19252  gsum2d2lem  19948  gsum2d2  19949  gsumcom2  19950  gsumxp  19951  dprd2d2  20021  mattpostpos  22419  mdetunilem9  22585  restbas  23123  txuni2  23530  txcls  23569  txdis1cn  23600  txkgen  23617  hmpher  23749  cnextrel  24028  tgphaus  24082  qustgplem  24086  tsmsxp  24120  utop2nei  24215  utop3cls  24216  xmeter  24398  caubl  25275  ovoliunlem1  25469  reldv  25837  taylf  26326  lgsquadlem1  27343  lgsquadlem2  27344  noseqrdgfn  28298  nvrel  30673  dfcnv2  32748  gsumpart  33124  gsumwrd2dccat  33139  elrgspnsubrunlem2  33309  qusxpid  33423  opprabs  33542  qtophaus  33980  cvmliftlem1  35467  cvmlift2lem12  35496  gonan0  35574  xpab  35908  dfso2  35937  relbigcup  36077  poimirlem3  37944  heicant  37976  vvdifopab  38586  cnvref4  38671  ecxrn2  38729  dvhopellsm  41563  dibvalrel  41609  dib1dim  41611  diclspsn  41640  dih1  41732  dih1dimatlem  41775  aoprssdm  47650  gricrel  48395  grlicrel  48482  eliunxp2  48810  iinxp  49306  coxp  49308  xpco2  49332  tposresxp  49358  tposf1o  49359  tposideq2  49364  joindm2  49443  meetdm2  49445  oppfvallem  49610  funcoppc3  49622  uptposlem  49672  reldmxpc  49721