Theorem relxp 5677

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

This proof depends on syntax axioms:  Vcvv 3453   ⊆ wss 3902   × cxp 5657  Rel wrel 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-opab 5172  df-xp 5665  df-rel 5666

This theorem is used by:  xpsspw  5794  relinxp  5799  inxp  5816  xpiindi  5819  eliunxp  5821  opeliunxp2  5822  relres  6002  restidsing  6053  codir  6118  qfto  6119  cnvxp  6152  difxp  6160  sofld  6184  cnvcnv  6189  dfco2  6245  unixp  6284  ressn  6287  fliftcnv  7316  fliftfun  7317  oprssdm  7599  frxp  8128  frxp2  8146  frxp3  8153  opeliunxp2f  8212  reltpos  8233  tposfo  8255  tposf  8256  swoer  8732  xpider  8792  xpcomf1o  9068  fpwwe2lem8  10651  ordpinq  10956  addassnq  10971  mulassnq  10972  distrnq  10974  mulidnq  10976  recmulnq  10977  ltexnq  10988  prcdnq  11006  ltrel  11299  lerel  11301  dfle2  13202  fsumcom2  15864  fprodcom2  16077  0rest  17520  firest  17523  2oppchomf  17818  isinv  17855  invsym2  17858  invfun  17859  oppcsect2  17874  oppcinv  17875  oppchofcl  18354  oyoncl  18364  clatl  18602  qusxpid  19314  gicer  19410  gsum2d2lem  20106  gsum2d2  20107  gsumcom2  20108  gsumxp  20109  dprd2d2  20179  ricrel  20661  mattpostpos  22682  mdetunilem9  22848  restbas  23389  txuni2  23797  txcls  23836  txdis1cn  23867  txkgen  23884  hmpher  24016  cnextrel  24295  tgphaus  24349  qustgplem  24353  tsmsxp  24387  utop2nei  24482  utop3cls  24483  xmeter  24665  caubl  25542  ovoliunlem1  25736  reldv  26104  taylf  26604  lgsquadlem1  27624  lgsquadlem2  27625  noseqrdgfn  28579  nvrel  31091  dfcnv2  33156  gsumpart  33511  gsumwrd2dccat  33526  elrgspnsubrunlem2  33696  opprabs  33892  qtophaus  34354  cvmliftlem1  35872  cvmlift2lem12  35901  gonan0  35979  xpab  36313  dfso2  36342  relbigcup  36482  poimirlem3  38380  heicant  38412  vvdifopab  39021  cnvref4  39106  ecxrn2  39164  dvhopellsm  41998  dibvalrel  42044  dib1dim  42046  diclspsn  42075  dih1  42167  dih1dimatlem  42210  aoprssdm  48098  gricrel  48843  grlicrel  48930  eliunxp2  49272  iinxp  49767  coxp  49769  xpco2  49793  tposresxp  49817  tposf1o  49818  tposideq2  49823  joindm2  49902  meetdm2  49904  oppfvallem  50069  funcoppc3  50081  uptposlem  50131  reldmxpc  50180