Theorem relxp 5266

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

Syntax hints:  Vcvv 3349   ⊆ wss 3721   × cxp 5247  Rel wrel 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-in 3728  df-ss 3735  df-opab 4845  df-xp 5255  df-rel 5256

This theorem is referenced by:  xpsspw  5372  xpiindi  5396  eliunxp  5398  opeliunxp2  5399  relres  5567  restidsing  5599  restidsingOLD  5600  codir  5657  qfto  5658  difxp  5699  sofld  5722  cnvcnv  5727  cnvcnvOLD  5728  dfco2  5778  unixp  5812  ressn  5815  fliftcnv  6703  fliftfun  6704  oprssdm  6961  frxp  7437  opeliunxp2f  7487  reltpos  7508  tpostpos  7523  tposfo  7530  tposf  7531  swoer  7925  xpider  7969  erinxp  7972  xpcomf1o  8204  cda1dif  9199  brdom3  9551  brdom5  9552  brdom4  9553  fpwwe2lem8  9660  fpwwe2lem9  9661  fpwwe2lem12  9664  ordpinq  9966  addassnq  9981  mulassnq  9982  distrnq  9984  mulidnq  9986  recmulnq  9987  ltexnq  9998  prcdnq  10016  ltrel  10301  lerel  10303  dfle2  12184  fsumcom2  14712  fprodcom2  14920  0rest  16297  firest  16300  pwsle  16359  2oppchomf  16590  isinv  16626  invsym2  16629  invfun  16630  oppcsect2  16645  oppcinv  16646  oppchofcl  17107  oyoncl  17117  clatl  17323  gicer  17925  gsum2d2lem  18578  gsum2d2  18579  gsumcom2  18580  gsumxp  18581  dprd2d2  18650  opsrtoslem2  19699  mattpostpos  20477  mdetunilem9  20643  restbas  21182  txuni2  21588  txcls  21627  txdis1cn  21658  txkgen  21675  hmpher  21807  cnextrel  22086  tgphaus  22139  qustgplem  22143  tsmsxp  22177  utop2nei  22273  utop3cls  22274  xmeter  22457  caubl  23324  ovoliunlem1  23489  reldv  23853  taylf  24334  lgsquadlem1  25325  lgsquadlem2  25326  nvrel  27791  dfcnv2  29810  qtophaus  30237  cvmliftlem1  31599  cvmlift2lem12  31628  dfso2  31976  elrn3  31984  relbigcup  32335  poimirlem3  33738  heicant  33770  vvdifopab  34360  inxprnres  34396  relinxp  34405  dvhopellsm  36920  dibvalrel  36966  dib1dim  36968  diclspsn  36997  dih1  37089  dih1dimatlem  37132  aoprssdm  41796  eliunxp2  42630