Theorem relxp 5639

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

Syntax hints:  Vcvv 3437   ⊆ wss 3898   × cxp 5619  Rel wrel 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-opab 5158  df-xp 5627  df-rel 5628

This theorem is referenced by:  xpsspw  5755  relinxp  5760  inxp  5777  xpiindi  5781  eliunxp  5783  opeliunxp2  5784  relres  5960  restidsing  6008  codir  6073  qfto  6074  difxp  6118  sofld  6141  cnvcnv  6146  dfco2  6199  unixp  6236  ressn  6239  fliftcnv  7253  fliftfun  7254  oprssdm  7535  frxp  8064  frxp2  8082  frxp3  8089  opeliunxp2f  8148  reltpos  8169  tposfo  8191  tposf  8192  swoer  8661  xpider  8720  xpcomf1o  8988  fpwwe2lem8  10538  ordpinq  10843  addassnq  10858  mulassnq  10859  distrnq  10861  mulidnq  10863  recmulnq  10864  ltexnq  10875  prcdnq  10893  ltrel  11183  lerel  11185  dfle2  13050  fsumcom2  15685  fprodcom2  15895  0rest  17337  firest  17340  2oppchomf  17634  isinv  17671  invsym2  17674  invfun  17675  oppcsect2  17690  oppcinv  17691  oppchofcl  18170  oyoncl  18180  clatl  18418  gicer  19193  gsum2d2lem  19889  gsum2d2  19890  gsumcom2  19891  gsumxp  19892  dprd2d2  19962  mattpostpos  22372  mdetunilem9  22538  restbas  23076  txuni2  23483  txcls  23522  txdis1cn  23553  txkgen  23570  hmpher  23702  cnextrel  23981  tgphaus  24035  qustgplem  24039  tsmsxp  24073  utop2nei  24168  utop3cls  24169  xmeter  24351  caubl  25238  ovoliunlem1  25433  reldv  25801  taylf  26298  lgsquadlem1  27321  lgsquadlem2  27322  noseqrdgfn  28239  nvrel  30586  dfcnv2  32662  gsumpart  33046  gsumwrd2dccat  33056  elrgspnsubrunlem2  33224  qusxpid  33337  opprabs  33456  qtophaus  33872  cvmliftlem1  35352  cvmlift2lem12  35381  gonan0  35459  xpab  35793  dfso2  35822  relbigcup  35962  poimirlem3  37686  heicant  37718  vvdifopab  38320  cnvref4  38405  ecxrn2  38455  dvhopellsm  41239  dibvalrel  41285  dib1dim  41287  diclspsn  41316  dih1  41408  dih1dimatlem  41451  aoprssdm  47329  gricrel  48046  grlicrel  48133  eliunxp2  48461  iinxp  48958  coxp  48960  xpco2  48984  tposresxp  49010  tposf1o  49011  tposideq2  49016  joindm2  49095  meetdm2  49097  oppfvallem  49263  funcoppc3  49275  uptposlem  49325  reldmxpc  49374