Theorem relxp 5669

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

This proof depends on syntax axioms:  Vcvv 3451   ⊆ wss 3899   × cxp 5649  Rel wrel 5656

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  xpsspw  5787  relinxp  5792  inxp  5809  xpiindi  5812  eliunxp  5814  opeliunxp2  5815  relres  5996  restidsing  6047  codir  6112  qfto  6113  cnvxp  6146  difxp  6154  sofld  6178  cnvcnv  6183  dfco2  6239  unixp  6278  ressn  6281  fliftcnv  7311  fliftfun  7312  oprssdm  7594  frxp  8127  frxp2  8145  frxp3  8152  opeliunxp2f  8211  reltpos  8232  tposfo  8254  tposf  8255  swoer  8733  xpider  8793  xpcomf1o  9069  fpwwe2lem8  10704  ordpinq  11009  addassnq  11024  mulassnq  11025  distrnq  11027  mulidnq  11029  recmulnq  11030  ltexnq  11041  prcdnq  11059  ltrel  11352  lerel  11354  dfle2  13257  fsumcom2  15920  fprodcom2  16131  0rest  17580  firest  17583  2oppchomf  17878  isinv  17915  invsym2  17918  invfun  17919  oppcsect2  17934  oppcinv  17935  oppchofcl  18414  oyoncl  18424  clatl  18662  qusxpid  19375  gicer  19471  gsum2d2lem  20167  gsum2d2  20168  gsumcom2  20169  gsumxp  20170  dprd2d2  20240  ricrel  20724  mattpostpos  22749  mdetunilem9  22915  restbas  23456  txuni2  23864  txcls  23903  txdis1cn  23934  txkgen  23951  hmpher  24083  cnextrel  24362  tgphaus  24416  qustgplem  24420  tsmsxp  24454  utop2nei  24549  utop3cls  24550  xmeter  24732  caubl  25609  ovoliunlem1  25803  reldv  26170  taylf  26670  lgsquadlem1  27689  lgsquadlem2  27690  noseqrdgfn  28674  nvrel  31186  dfcnv2  33251  gsumpart  33606  gsumwrd2dccat  33621  elrgspnsubrunlem2  33791  opprabs  33988  qtophaus  34450  cvmliftlem1  36019  cvmlift2lem12  36048  gonan0  36126  xpab  36460  dfso2  36489  relbigcup  36629  poimirlem3  38509  heicant  38541  vvdifopab  39165  cnvref4  39250  ecxrn2  39308  dvhopellsm  42142  dibvalrel  42188  dib1dim  42190  diclspsn  42219  dih1  42311  dih1dimatlem  42354  aoprssdm  48216  gricrel  48961  grlicrel  49048  eliunxp2  49390  iinxp  49885  coxp  49887  xpco2  49911  tposresxp  49935  tposf1o  49936  tposideq2  49941  joindm2  50020  meetdm2  50022  oppfvallem  50187  funcoppc3  50199  uptposlem  50249  reldmxpc  50298