Theorem relxp 5693

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

Syntax hints:  Vcvv 3474   ⊆ wss 3947   × cxp 5673  Rel wrel 5680

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-opab 5210  df-xp 5681  df-rel 5682

This theorem is referenced by:  xpsspw  5807  relinxp  5812  xpiindi  5833  eliunxp  5835  opeliunxp2  5836  relres  6008  restidsing  6050  codir  6118  qfto  6119  difxp  6160  sofld  6183  cnvcnv  6188  dfco2  6241  unixp  6278  ressn  6281  fliftcnv  7304  fliftfun  7305  oprssdm  7584  frxp  8108  frxp2  8126  frxp3  8133  opeliunxp2f  8191  reltpos  8212  tposfo  8234  tposf  8235  swoer  8729  xpider  8778  xpcomf1o  9057  fpwwe2lem8  10629  ordpinq  10934  addassnq  10949  mulassnq  10950  distrnq  10952  mulidnq  10954  recmulnq  10955  ltexnq  10966  prcdnq  10984  ltrel  11272  lerel  11274  dfle2  13122  fsumcom2  15716  fprodcom2  15924  0rest  17371  firest  17374  2oppchomf  17666  isinv  17703  invsym2  17706  invfun  17707  oppcsect2  17722  oppcinv  17723  oppchofcl  18209  oyoncl  18219  clatl  18457  gicer  19144  gsum2d2lem  19835  gsum2d2  19836  gsumcom2  19837  gsumxp  19838  dprd2d2  19908  mattpostpos  21947  mdetunilem9  22113  restbas  22653  txuni2  23060  txcls  23099  txdis1cn  23130  txkgen  23147  hmpher  23279  cnextrel  23558  tgphaus  23612  qustgplem  23616  tsmsxp  23650  utop2nei  23746  utop3cls  23747  xmeter  23930  caubl  24816  ovoliunlem1  25010  reldv  25378  taylf  25864  lgsquadlem1  26872  lgsquadlem2  26873  nvrel  29842  dfcnv2  31888  gsumpart  32194  qusxpid  32463  opprabs  32584  qtophaus  32804  cvmliftlem1  34264  cvmlift2lem12  34293  gonan0  34371  xpab  34683  dfso2  34713  relbigcup  34857  poimirlem3  36479  heicant  36511  vvdifopab  37116  cnvref4  37207  dvhopellsm  39976  dibvalrel  40022  dib1dim  40024  diclspsn  40053  dih1  40145  dih1dimatlem  40188  aoprssdm  45896  eliunxp2  46962  joindm2  47554  meetdm2  47556