Theorem relxp 5643

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

Syntax hints:  Vcvv 3432   ⊆ wss 3890   × cxp 5623  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-opab 5142  df-xp 5631  df-rel 5632

This theorem is referenced by:  xpsspw  5759  relinxp  5764  inxp  5781  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  7262  fliftfun  7263  oprssdm  7544  frxp  8073  frxp2  8091  frxp3  8098  opeliunxp2f  8157  reltpos  8178  tposfo  8200  tposf  8201  swoer  8672  xpider  8732  xpcomf1o  9001  fpwwe2lem8  10559  ordpinq  10864  addassnq  10879  mulassnq  10880  distrnq  10882  mulidnq  10884  recmulnq  10885  ltexnq  10896  prcdnq  10914  ltrel  11205  lerel  11207  dfle2  13096  fsumcom2  15734  fprodcom2  15947  0rest  17390  firest  17393  2oppchomf  17688  isinv  17725  invsym2  17728  invfun  17729  oppcsect2  17744  oppcinv  17745  oppchofcl  18224  oyoncl  18234  clatl  18472  gicer  19250  gsum2d2lem  19946  gsum2d2  19947  gsumcom2  19948  gsumxp  19949  dprd2d2  20019  mattpostpos  22444  mdetunilem9  22610  restbas  23148  txuni2  23555  txcls  23594  txdis1cn  23625  txkgen  23642  hmpher  23774  cnextrel  24053  tgphaus  24107  qustgplem  24111  tsmsxp  24145  utop2nei  24240  utop3cls  24241  xmeter  24423  caubl  25300  ovoliunlem1  25494  reldv  25862  taylf  26351  lgsquadlem1  27368  lgsquadlem2  27369  noseqrdgfn  28323  nvrel  30698  dfcnv2  32774  gsumpart  33151  gsumwrd2dccat  33166  elrgspnsubrunlem2  33336  qusxpid  33453  opprabs  33572  qtophaus  34027  cvmliftlem1  35520  cvmlift2lem12  35549  gonan0  35627  xpab  35961  dfso2  35990  relbigcup  36130  poimirlem3  37997  heicant  38029  vvdifopab  38639  cnvref4  38724  ecxrn2  38782  dvhopellsm  41616  dibvalrel  41662  dib1dim  41664  diclspsn  41693  dih1  41785  dih1dimatlem  41828  aoprssdm  47672  gricrel  48417  grlicrel  48504  eliunxp2  48832  iinxp  49328  coxp  49330  xpco2  49354  tposresxp  49380  tposf1o  49381  tposideq2  49386  joindm2  49465  meetdm2  49467  oppfvallem  49632  funcoppc3  49644  uptposlem  49694  reldmxpc  49743