Theorem relxp 5542

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

Syntax hints:  Vcvv 3409   ⊆ wss 3858   × cxp 5522  Rel wrel 5529

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-opab 5095  df-xp 5530  df-rel 5531

This theorem is referenced by:  xpsspw  5651  relinxp  5656  xpiindi  5675  eliunxp  5677  opeliunxp2  5678  relres  5852  restidsing  5894  codir  5952  qfto  5953  difxp  5993  sofld  6016  cnvcnv  6021  dfco2  6075  unixp  6111  ressn  6114  fliftcnv  7058  fliftfun  7059  oprssdm  7325  frxp  7825  opeliunxp2f  7886  reltpos  7907  tposfo  7929  tposf  7930  swoer  8329  xpider  8378  xpcomf1o  8627  fpwwe2lem8  10098  ordpinq  10403  addassnq  10418  mulassnq  10419  distrnq  10421  mulidnq  10423  recmulnq  10424  ltexnq  10435  prcdnq  10453  ltrel  10741  lerel  10743  dfle2  12581  fsumcom2  15177  fprodcom2  15386  0rest  16761  firest  16764  2oppchomf  17052  isinv  17089  invsym2  17092  invfun  17093  oppcsect2  17108  oppcinv  17109  oppchofcl  17576  oyoncl  17586  clatl  17792  gicer  18483  gsum2d2lem  19161  gsum2d2  19162  gsumcom2  19163  gsumxp  19164  dprd2d2  19234  mattpostpos  21154  mdetunilem9  21320  restbas  21858  txuni2  22265  txcls  22304  txdis1cn  22335  txkgen  22352  hmpher  22484  cnextrel  22763  tgphaus  22817  qustgplem  22821  tsmsxp  22855  utop2nei  22951  utop3cls  22952  xmeter  23135  caubl  24008  ovoliunlem1  24202  reldv  24569  taylf  25055  lgsquadlem1  26063  lgsquadlem2  26064  nvrel  28484  dfcnv2  30537  gsumpart  30841  qusxpid  31080  qtophaus  31307  cvmliftlem1  32763  cvmlift2lem12  32792  gonan0  32870  xpab  33195  dfso2  33237  frxp2  33346  frxp3  33352  relbigcup  33748  poimirlem3  35340  heicant  35372  vvdifopab  35961  dvhopellsm  38693  dibvalrel  38739  dib1dim  38741  diclspsn  38770  dih1  38862  dih1dimatlem  38905  aoprssdm  44126  eliunxp2  45102