Theorem relxp 5650

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

Syntax hints:  Vcvv 3442   ⊆ wss 3903   × cxp 5630  Rel wrel 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-opab 5163  df-xp 5638  df-rel 5639

This theorem is referenced by:  xpsspw  5766  relinxp  5771  inxp  5788  xpiindi  5792  eliunxp  5794  opeliunxp2  5795  relres  5972  restidsing  6020  codir  6085  qfto  6086  difxp  6130  sofld  6153  cnvcnv  6158  dfco2  6211  unixp  6248  ressn  6251  fliftcnv  7267  fliftfun  7268  oprssdm  7549  frxp  8078  frxp2  8096  frxp3  8103  opeliunxp2f  8162  reltpos  8183  tposfo  8205  tposf  8206  swoer  8677  xpider  8737  xpcomf1o  9006  fpwwe2lem8  10561  ordpinq  10866  addassnq  10881  mulassnq  10882  distrnq  10884  mulidnq  10886  recmulnq  10887  ltexnq  10898  prcdnq  10916  ltrel  11206  lerel  11208  dfle2  13073  fsumcom2  15709  fprodcom2  15919  0rest  17361  firest  17364  2oppchomf  17659  isinv  17696  invsym2  17699  invfun  17700  oppcsect2  17715  oppcinv  17716  oppchofcl  18195  oyoncl  18205  clatl  18443  gicer  19218  gsum2d2lem  19914  gsum2d2  19915  gsumcom2  19916  gsumxp  19917  dprd2d2  19987  mattpostpos  22410  mdetunilem9  22576  restbas  23114  txuni2  23521  txcls  23560  txdis1cn  23591  txkgen  23608  hmpher  23740  cnextrel  24019  tgphaus  24073  qustgplem  24077  tsmsxp  24111  utop2nei  24206  utop3cls  24207  xmeter  24389  caubl  25276  ovoliunlem1  25471  reldv  25839  taylf  26336  lgsquadlem1  27359  lgsquadlem2  27360  noseqrdgfn  28314  nvrel  30689  dfcnv2  32764  gsumpart  33156  gsumwrd2dccat  33171  elrgspnsubrunlem2  33341  qusxpid  33455  opprabs  33574  qtophaus  34013  cvmliftlem1  35498  cvmlift2lem12  35527  gonan0  35605  xpab  35939  dfso2  35968  relbigcup  36108  poimirlem3  37871  heicant  37903  vvdifopab  38513  cnvref4  38598  ecxrn2  38656  dvhopellsm  41490  dibvalrel  41536  dib1dim  41538  diclspsn  41567  dih1  41659  dih1dimatlem  41702  aoprssdm  47559  gricrel  48276  grlicrel  48363  eliunxp2  48691  iinxp  49187  coxp  49189  xpco2  49213  tposresxp  49239  tposf1o  49240  tposideq2  49245  joindm2  49324  meetdm2  49326  oppfvallem  49491  funcoppc3  49503  uptposlem  49553  reldmxpc  49602