Theorem relxp 5642

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

Syntax hints:  Vcvv 3440   ⊆ wss 3901   × cxp 5622  Rel wrel 5629

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-opab 5161  df-xp 5630  df-rel 5631

This theorem is referenced by:  xpsspw  5758  relinxp  5763  inxp  5780  xpiindi  5784  eliunxp  5786  opeliunxp2  5787  relres  5964  restidsing  6012  codir  6077  qfto  6078  difxp  6122  sofld  6145  cnvcnv  6150  dfco2  6203  unixp  6240  ressn  6243  fliftcnv  7257  fliftfun  7258  oprssdm  7539  frxp  8068  frxp2  8086  frxp3  8093  opeliunxp2f  8152  reltpos  8173  tposfo  8195  tposf  8196  swoer  8666  xpider  8725  xpcomf1o  8994  fpwwe2lem8  10549  ordpinq  10854  addassnq  10869  mulassnq  10870  distrnq  10872  mulidnq  10874  recmulnq  10875  ltexnq  10886  prcdnq  10904  ltrel  11194  lerel  11196  dfle2  13061  fsumcom2  15697  fprodcom2  15907  0rest  17349  firest  17352  2oppchomf  17647  isinv  17684  invsym2  17687  invfun  17688  oppcsect2  17703  oppcinv  17704  oppchofcl  18183  oyoncl  18193  clatl  18431  gicer  19206  gsum2d2lem  19902  gsum2d2  19903  gsumcom2  19904  gsumxp  19905  dprd2d2  19975  mattpostpos  22398  mdetunilem9  22564  restbas  23102  txuni2  23509  txcls  23548  txdis1cn  23579  txkgen  23596  hmpher  23728  cnextrel  24007  tgphaus  24061  qustgplem  24065  tsmsxp  24099  utop2nei  24194  utop3cls  24195  xmeter  24377  caubl  25264  ovoliunlem1  25459  reldv  25827  taylf  26324  lgsquadlem1  27347  lgsquadlem2  27348  noseqrdgfn  28302  nvrel  30677  dfcnv2  32754  gsumpart  33146  gsumwrd2dccat  33160  elrgspnsubrunlem2  33330  qusxpid  33444  opprabs  33563  qtophaus  33993  cvmliftlem1  35479  cvmlift2lem12  35508  gonan0  35586  xpab  35920  dfso2  35949  relbigcup  36089  poimirlem3  37824  heicant  37856  vvdifopab  38458  cnvref4  38543  ecxrn2  38593  dvhopellsm  41377  dibvalrel  41423  dib1dim  41425  diclspsn  41454  dih1  41546  dih1dimatlem  41589  aoprssdm  47448  gricrel  48165  grlicrel  48252  eliunxp2  48580  iinxp  49076  coxp  49078  xpco2  49102  tposresxp  49128  tposf1o  49129  tposideq2  49134  joindm2  49213  meetdm2  49215  oppfvallem  49380  funcoppc3  49392  uptposlem  49442  reldmxpc  49491