Theorem relxp 5227

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

Syntax hints:  Vcvv 3200   ⊆ wss 3574   × cxp 5112  Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-opab 4713  df-xp 5120  df-rel 5121

This theorem is referenced by:  xpsspw  5233  xpiindi  5257  eliunxp  5259  opeliunxp2  5260  relres  5426  restidsing  5458  restidsingOLD  5459  codir  5516  qfto  5517  difxp  5558  sofld  5581  cnvcnv  5586  cnvcnvOLD  5587  dfco2  5634  unixp  5668  ressn  5671  fliftcnv  6561  fliftfun  6562  oprssdm  6815  frxp  7287  opeliunxp2f  7336  reltpos  7357  tpostpos  7372  tposfo  7379  tposf  7380  swoer  7772  xpider  7818  erinxp  7821  xpcomf1o  8049  cda1dif  8998  brdom3  9350  brdom5  9351  brdom4  9352  fpwwe2lem8  9459  fpwwe2lem9  9460  fpwwe2lem12  9463  ordpinq  9765  addassnq  9780  mulassnq  9781  distrnq  9783  mulidnq  9785  recmulnq  9786  ltexnq  9797  prcdnq  9815  ltrel  10100  lerel  10102  dfle2  11980  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  0rest  16090  firest  16093  pwsle  16152  2oppchomf  16384  isinv  16420  invsym2  16423  invfun  16424  oppcsect2  16439  oppcinv  16440  oppchofcl  16900  oyoncl  16910  clatl  17116  gicer  17718  gicerOLD  17719  gsum2d2lem  18372  gsum2d2  18373  gsumcom2  18374  gsumxp  18375  dprd2d2  18443  opsrtoslem2  19485  mattpostpos  20260  mdetunilem9  20426  restbas  20962  txuni2  21368  txcls  21407  txdis1cn  21438  txkgen  21455  hmpher  21587  cnextrel  21867  tgphaus  21920  qustgplem  21924  tsmsxp  21958  utop2nei  22054  utop3cls  22055  xmeter  22238  caubl  23106  ovoliunlem1  23270  reldv  23634  taylf  24115  lgsquadlem1  25105  lgsquadlem2  25106  nvrel  27457  dfcnv2  29476  qtophaus  29903  cvmliftlem1  31267  cvmlift2lem12  31296  dfso2  31644  elrn3  31652  relbigcup  32004  poimirlem3  33412  heicant  33444  vvdifopab  34024  inxprnres  34060  relinxp  34069  dvhopellsm  36406  dibvalrel  36452  dib1dim  36454  diclspsn  36483  dih1  36575  dih1dimatlem  36618  aoprssdm  41282  eliunxp2  42112