Theorem relxp 5566

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

Syntax hints:  Vcvv 3493   ⊆ wss 3934   × cxp 5546  Rel wrel 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-in 3941  df-ss 3950  df-opab 5120  df-xp 5554  df-rel 5555

This theorem is referenced by:  xpsspw  5675  relinxp  5680  xpiindi  5699  eliunxp  5701  opeliunxp2  5702  relres  5875  restidsing  5915  codir  5973  qfto  5974  difxp  6014  sofld  6037  cnvcnv  6042  dfco2  6091  unixp  6126  ressn  6129  fliftcnv  7056  fliftfun  7057  oprssdm  7321  frxp  7812  opeliunxp2f  7868  reltpos  7889  tposfo  7911  tposf  7912  swoer  8311  xpider  8360  xpcomf1o  8598  fpwwe2lem9  10052  ordpinq  10357  addassnq  10372  mulassnq  10373  distrnq  10375  mulidnq  10377  recmulnq  10378  ltexnq  10389  prcdnq  10407  ltrel  10695  lerel  10697  dfle2  12532  fsumcom2  15121  fprodcom2  15330  0rest  16695  firest  16698  2oppchomf  16986  isinv  17022  invsym2  17025  invfun  17026  oppcsect2  17041  oppcinv  17042  oppchofcl  17502  oyoncl  17512  clatl  17718  gicer  18408  gsum2d2lem  19085  gsum2d2  19086  gsumcom2  19087  gsumxp  19088  dprd2d2  19158  mattpostpos  21055  mdetunilem9  21221  restbas  21758  txuni2  22165  txcls  22204  txdis1cn  22235  txkgen  22252  hmpher  22384  cnextrel  22663  tgphaus  22717  qustgplem  22721  tsmsxp  22755  utop2nei  22851  utop3cls  22852  xmeter  23035  caubl  23903  ovoliunlem1  24095  reldv  24460  taylf  24941  lgsquadlem1  25948  lgsquadlem2  25949  nvrel  28371  dfcnv2  30414  qusxpid  30921  qtophaus  31093  cvmliftlem1  32525  cvmlift2lem12  32554  gonan0  32632  dfso2  32983  relbigcup  33351  poimirlem3  34887  heicant  34919  vvdifopab  35513  dvhopellsm  38245  dibvalrel  38291  dib1dim  38293  diclspsn  38322  dih1  38414  dih1dimatlem  38457  aoprssdm  43391  eliunxp2  44372