Theorem relxp 5634

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

Syntax hints:  Vcvv 3436   ⊆ wss 3902   × cxp 5614  Rel wrel 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-opab 5154  df-xp 5622  df-rel 5623

This theorem is referenced by:  xpsspw  5749  relinxp  5754  inxp  5771  xpiindi  5775  eliunxp  5777  opeliunxp2  5778  relres  5954  restidsing  6002  codir  6067  qfto  6068  difxp  6111  sofld  6134  cnvcnv  6139  dfco2  6192  unixp  6229  ressn  6232  fliftcnv  7245  fliftfun  7246  oprssdm  7527  frxp  8056  frxp2  8074  frxp3  8081  opeliunxp2f  8140  reltpos  8161  tposfo  8183  tposf  8184  swoer  8653  xpider  8712  xpcomf1o  8979  fpwwe2lem8  10529  ordpinq  10834  addassnq  10849  mulassnq  10850  distrnq  10852  mulidnq  10854  recmulnq  10855  ltexnq  10866  prcdnq  10884  ltrel  11174  lerel  11176  dfle2  13046  fsumcom2  15681  fprodcom2  15891  0rest  17333  firest  17336  2oppchomf  17630  isinv  17667  invsym2  17670  invfun  17671  oppcsect2  17686  oppcinv  17687  oppchofcl  18166  oyoncl  18176  clatl  18414  gicer  19190  gsum2d2lem  19886  gsum2d2  19887  gsumcom2  19888  gsumxp  19889  dprd2d2  19959  mattpostpos  22370  mdetunilem9  22536  restbas  23074  txuni2  23481  txcls  23520  txdis1cn  23551  txkgen  23568  hmpher  23700  cnextrel  23979  tgphaus  24033  qustgplem  24037  tsmsxp  24071  utop2nei  24166  utop3cls  24167  xmeter  24349  caubl  25236  ovoliunlem1  25431  reldv  25799  taylf  26296  lgsquadlem1  27319  lgsquadlem2  27320  noseqrdgfn  28237  nvrel  30580  dfcnv2  32656  gsumpart  33035  gsumwrd2dccat  33045  elrgspnsubrunlem2  33213  qusxpid  33326  opprabs  33445  qtophaus  33847  cvmliftlem1  35327  cvmlift2lem12  35356  gonan0  35434  xpab  35768  dfso2  35797  relbigcup  35937  poimirlem3  37669  heicant  37701  vvdifopab  38301  cnvref4  38384  dvhopellsm  41162  dibvalrel  41208  dib1dim  41210  diclspsn  41239  dih1  41331  dih1dimatlem  41374  aoprssdm  47239  gricrel  47956  grlicrel  48043  eliunxp2  48371  iinxp  48868  coxp  48870  xpco2  48894  tposresxp  48920  tposf1o  48921  tposideq2  48926  joindm2  49005  meetdm2  49007  oppfvallem  49173  funcoppc3  49185  uptposlem  49235  reldmxpc  49284