Theorem relxp 5718

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

Syntax hints:  Vcvv 3488   ⊆ wss 3976   × cxp 5698  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  xpsspw  5833  relinxp  5838  inxp  5856  xpiindi  5860  eliunxp  5862  opeliunxp2  5863  relres  6035  restidsing  6082  codir  6152  qfto  6153  difxp  6195  sofld  6218  cnvcnv  6223  dfco2  6276  unixp  6313  ressn  6316  fliftcnv  7347  fliftfun  7348  oprssdm  7631  frxp  8167  frxp2  8185  frxp3  8192  opeliunxp2f  8251  reltpos  8272  tposfo  8294  tposf  8295  swoer  8794  xpider  8846  xpcomf1o  9127  fpwwe2lem8  10707  ordpinq  11012  addassnq  11027  mulassnq  11028  distrnq  11030  mulidnq  11032  recmulnq  11033  ltexnq  11044  prcdnq  11062  ltrel  11352  lerel  11354  dfle2  13209  fsumcom2  15822  fprodcom2  16032  0rest  17489  firest  17492  2oppchomf  17784  isinv  17821  invsym2  17824  invfun  17825  oppcsect2  17840  oppcinv  17841  oppchofcl  18330  oyoncl  18340  clatl  18578  gicer  19317  gsum2d2lem  20015  gsum2d2  20016  gsumcom2  20017  gsumxp  20018  dprd2d2  20088  mattpostpos  22481  mdetunilem9  22647  restbas  23187  txuni2  23594  txcls  23633  txdis1cn  23664  txkgen  23681  hmpher  23813  cnextrel  24092  tgphaus  24146  qustgplem  24150  tsmsxp  24184  utop2nei  24280  utop3cls  24281  xmeter  24464  caubl  25361  ovoliunlem1  25556  reldv  25925  taylf  26420  lgsquadlem1  27442  lgsquadlem2  27443  noseqrdgfn  28330  nvrel  30634  dfcnv2  32694  gsumpart  33038  qusxpid  33356  opprabs  33475  qtophaus  33782  cvmliftlem1  35253  cvmlift2lem12  35282  gonan0  35360  xpab  35688  dfso2  35717  relbigcup  35861  poimirlem3  37583  heicant  37615  vvdifopab  38216  cnvref4  38306  dvhopellsm  41074  dibvalrel  41120  dib1dim  41122  diclspsn  41151  dih1  41243  dih1dimatlem  41286  aoprssdm  47117  gricrel  47772  grlicrel  47823  eliunxp2  48058  joindm2  48648  meetdm2  48650