Theorem relxp 5695

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

Syntax hints:  Vcvv 3475   ⊆ wss 3949   × cxp 5675  Rel wrel 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684

This theorem is referenced by:  xpsspw  5810  relinxp  5815  xpiindi  5836  eliunxp  5838  opeliunxp2  5839  relres  6011  restidsing  6053  codir  6122  qfto  6123  difxp  6164  sofld  6187  cnvcnv  6192  dfco2  6245  unixp  6282  ressn  6285  fliftcnv  7308  fliftfun  7309  oprssdm  7588  frxp  8112  frxp2  8130  frxp3  8137  opeliunxp2f  8195  reltpos  8216  tposfo  8238  tposf  8239  swoer  8733  xpider  8782  xpcomf1o  9061  fpwwe2lem8  10633  ordpinq  10938  addassnq  10953  mulassnq  10954  distrnq  10956  mulidnq  10958  recmulnq  10959  ltexnq  10970  prcdnq  10988  ltrel  11276  lerel  11278  dfle2  13126  fsumcom2  15720  fprodcom2  15928  0rest  17375  firest  17378  2oppchomf  17670  isinv  17707  invsym2  17710  invfun  17711  oppcsect2  17726  oppcinv  17727  oppchofcl  18213  oyoncl  18223  clatl  18461  gicer  19150  gsum2d2lem  19841  gsum2d2  19842  gsumcom2  19843  gsumxp  19844  dprd2d2  19914  mattpostpos  21956  mdetunilem9  22122  restbas  22662  txuni2  23069  txcls  23108  txdis1cn  23139  txkgen  23156  hmpher  23288  cnextrel  23567  tgphaus  23621  qustgplem  23625  tsmsxp  23659  utop2nei  23755  utop3cls  23756  xmeter  23939  caubl  24825  ovoliunlem1  25019  reldv  25387  taylf  25873  lgsquadlem1  26883  lgsquadlem2  26884  nvrel  29855  dfcnv2  31901  gsumpart  32207  qusxpid  32475  opprabs  32596  qtophaus  32816  cvmliftlem1  34276  cvmlift2lem12  34305  gonan0  34383  xpab  34695  dfso2  34725  relbigcup  34869  poimirlem3  36491  heicant  36523  vvdifopab  37128  cnvref4  37219  dvhopellsm  39988  dibvalrel  40034  dib1dim  40036  diclspsn  40065  dih1  40157  dih1dimatlem  40200  aoprssdm  45910  eliunxp2  47009  joindm2  47601  meetdm2  47603