Theorem relxp 5659

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

Syntax hints:  Vcvv 3450   ⊆ wss 3917   × cxp 5639  Rel wrel 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  xpsspw  5775  relinxp  5780  inxp  5798  xpiindi  5802  eliunxp  5804  opeliunxp2  5805  relres  5979  restidsing  6027  codir  6096  qfto  6097  difxp  6140  sofld  6163  cnvcnv  6168  dfco2  6221  unixp  6258  ressn  6261  fliftcnv  7289  fliftfun  7290  oprssdm  7573  frxp  8108  frxp2  8126  frxp3  8133  opeliunxp2f  8192  reltpos  8213  tposfo  8235  tposf  8236  swoer  8705  xpider  8764  xpcomf1o  9035  fpwwe2lem8  10598  ordpinq  10903  addassnq  10918  mulassnq  10919  distrnq  10921  mulidnq  10923  recmulnq  10924  ltexnq  10935  prcdnq  10953  ltrel  11243  lerel  11245  dfle2  13114  fsumcom2  15747  fprodcom2  15957  0rest  17399  firest  17402  2oppchomf  17692  isinv  17729  invsym2  17732  invfun  17733  oppcsect2  17748  oppcinv  17749  oppchofcl  18228  oyoncl  18238  clatl  18474  gicer  19216  gsum2d2lem  19910  gsum2d2  19911  gsumcom2  19912  gsumxp  19913  dprd2d2  19983  mattpostpos  22348  mdetunilem9  22514  restbas  23052  txuni2  23459  txcls  23498  txdis1cn  23529  txkgen  23546  hmpher  23678  cnextrel  23957  tgphaus  24011  qustgplem  24015  tsmsxp  24049  utop2nei  24145  utop3cls  24146  xmeter  24328  caubl  25215  ovoliunlem1  25410  reldv  25778  taylf  26275  lgsquadlem1  27298  lgsquadlem2  27299  noseqrdgfn  28207  nvrel  30538  dfcnv2  32607  gsumpart  33004  gsumwrd2dccat  33014  elrgspnsubrunlem2  33206  qusxpid  33341  opprabs  33460  qtophaus  33833  cvmliftlem1  35279  cvmlift2lem12  35308  gonan0  35386  xpab  35720  dfso2  35749  relbigcup  35892  poimirlem3  37624  heicant  37656  vvdifopab  38256  cnvref4  38339  dvhopellsm  41118  dibvalrel  41164  dib1dim  41166  diclspsn  41195  dih1  41287  dih1dimatlem  41330  aoprssdm  47207  gricrel  47923  grlicrel  48002  eliunxp2  48326  iinxp  48823  coxp  48825  xpco2  48849  tposresxp  48875  tposf1o  48876  tposideq2  48881  joindm2  48960  meetdm2  48962  oppfvallem  49128  funcoppc3  49140  uptposlem  49190  reldmxpc  49239