Theorem relxp 5674

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

This proof depends on syntax axioms:  Vcvv 3454   ⊆ wss 3900   × cxp 5654  Rel wrel 5661

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-opab 5172  df-xp 5662  df-rel 5663

This theorem is used by:  xpsspw  5793  relinxp  5798  inxp  5816  xpiindi  5819  eliunxp  5821  opeliunxp2  5822  relresOLD  6009  restidsing  6058  codir  6127  qfto  6128  cnvxp  6160  difxp  6168  sofld  6192  cnvcnv  6197  dfco2  6260  unixp  6304  ressn  6307  fliftcnv  7345  fliftfun  7346  oprssdm  7629  frxp  8168  frxp2  8191  frxp3  8198  opeliunxp2f  8258  reltpos  8279  tposfo  8301  tposf  8302  swoer  8780  xpider  8840  xpcomf1o  9116  fpwwe2lem8  10753  ordpinq  11058  addassnq  11073  mulassnq  11074  distrnq  11076  mulidnq  11078  recmulnq  11079  ltexnq  11090  prcdnq  11108  ltrel  11401  lerel  11403  dfle2  13306  fsumcom2  15972  fprodcom2  16183  0rest  17632  firest  17635  2oppchomf  17930  isinv  17967  invsym2  17970  invfun  17971  oppcsect2  17986  oppcinv  17987  oppchofcl  18466  oyoncl  18476  clatl  18714  qusxpid  19427  gicer  19524  gsum2d2lem  20220  gsum2d2  20221  gsumcom2  20222  gsumxp  20223  dprd2d2  20293  ricrel  20777  mattpostpos  22802  mdetunilem9  22968  restbas  23509  txuni2  23917  txcls  23956  txdis1cn  23987  txkgen  24004  hmpher  24136  cnextrel  24415  tgphaus  24469  qustgplem  24473  tsmsxp  24507  utop2nei  24602  utop3cls  24603  xmeter  24785  caubl  25662  ovoliunlem1  25856  reldv  26223  taylf  26721  lgsquadlem1  27740  lgsquadlem2  27741  noseqrdgfn  28725  nvrel  31237  dfcnv2  33343  gsumpart  33700  gsumwrd2dccat  33715  elrgspnsubrunlem2  33885  opprabs  34090  qtophaus  34551  cvmliftlem1  36230  cvmlift2lem12  36259  gonan0  36337  xpab  36682  dfso2  36711  relbigcup  36850  poimirlem3  38746  heicant  38778  vvdifopab  39400  cnvref4  39485  ecxrn2  39543  dvhopellsm  42377  dibvalrel  42423  dib1dim  42425  diclspsn  42454  dih1  42546  dih1dimatlem  42589  hfstructfun  46235  aoprssdm  48487  gricrel  49232  grlicrel  49319  eliunxp2  49661  iinxp  50157  coxp  50159  xpco2  50183  tposresxp  50211  tposf1o  50212  tposideq2  50217  joindm2  50297  meetdm2  50299  oppfvallem  50466  funcoppc3  50478  uptposlem  50528  reldmxpc  50583