Theorem relxp 5706

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

Syntax hints:  Vcvv 3477   ⊆ wss 3962   × cxp 5686  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  xpsspw  5821  relinxp  5826  inxp  5844  xpiindi  5848  eliunxp  5850  opeliunxp2  5851  relres  6025  restidsing  6072  codir  6142  qfto  6143  difxp  6185  sofld  6208  cnvcnv  6213  dfco2  6266  unixp  6303  ressn  6306  fliftcnv  7330  fliftfun  7331  oprssdm  7613  frxp  8149  frxp2  8167  frxp3  8174  opeliunxp2f  8233  reltpos  8254  tposfo  8276  tposf  8277  swoer  8774  xpider  8826  xpcomf1o  9099  fpwwe2lem8  10675  ordpinq  10980  addassnq  10995  mulassnq  10996  distrnq  10998  mulidnq  11000  recmulnq  11001  ltexnq  11012  prcdnq  11030  ltrel  11320  lerel  11322  dfle2  13185  fsumcom2  15806  fprodcom2  16016  0rest  17475  firest  17478  2oppchomf  17770  isinv  17807  invsym2  17810  invfun  17811  oppcsect2  17826  oppcinv  17827  oppchofcl  18316  oyoncl  18326  clatl  18565  gicer  19307  gsum2d2lem  20005  gsum2d2  20006  gsumcom2  20007  gsumxp  20008  dprd2d2  20078  mattpostpos  22475  mdetunilem9  22641  restbas  23181  txuni2  23588  txcls  23627  txdis1cn  23658  txkgen  23675  hmpher  23807  cnextrel  24086  tgphaus  24140  qustgplem  24144  tsmsxp  24178  utop2nei  24274  utop3cls  24275  xmeter  24458  caubl  25355  ovoliunlem1  25550  reldv  25919  taylf  26416  lgsquadlem1  27438  lgsquadlem2  27439  noseqrdgfn  28326  nvrel  30630  dfcnv2  32692  gsumpart  33042  gsumwrd2dccat  33052  qusxpid  33370  opprabs  33489  qtophaus  33796  cvmliftlem1  35269  cvmlift2lem12  35298  gonan0  35376  xpab  35705  dfso2  35734  relbigcup  35878  poimirlem3  37609  heicant  37641  vvdifopab  38241  cnvref4  38331  dvhopellsm  41099  dibvalrel  41145  dib1dim  41147  diclspsn  41176  dih1  41268  dih1dimatlem  41311  aoprssdm  47151  gricrel  47825  grlicrel  47901  eliunxp2  48178  joindm2  48764  meetdm2  48766