Theorem relxp 5110

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 ( A X. B )

Proof of Theorem relxp

Step	Hyp	Ref	Expression
1		xpss 5109	. 2 |- ( A X. B ) C_ ( _V X. _V )
2		df-rel 5006	. 2 |- ( Rel ( A X. B ) <-> ( A X. B ) C_ ( _V X. _V ) )
3	1, 2	mpbir 209	1 |- Rel ( A X. B )

Syntax hints:   _Vcvv 3113   C_ wss 3476   X. cxp 4997   Rel wrel 5004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-opab 4506  df-xp 5005  df-rel 5006

This theorem is referenced by:  xpsspwOLD  5117  xpiindi  5138  eliunxp  5140  opeliunxp2  5141  relres  5301  restidsing  5330  codir  5387  qfto  5388  difxp  5431  sofld  5455  cnvcnv  5459  dfco2  5506  unixp  5540  ressn  5543  fliftcnv  6198  fliftfun  6199  oprssdm  6441  frxp  6894  reltpos  6961  tpostpos  6976  tposfo  6983  tposf  6984  swoer  7340  xpider  7383  erinxp  7386  xpcomf1o  7607  cda1dif  8557  brdom3  8907  brdom5  8908  brdom4  8909  fpwwe2lem8  9016  fpwwe2lem9  9017  fpwwe2lem12  9020  ordpinq  9322  addassnq  9337  mulassnq  9338  distrnq  9340  mulidnq  9342  recmulnq  9343  ltexnq  9354  prcdnq  9372  ltrel  9650  lerel  9652  dfle2  11354  fsumcom2  13555  0rest  14688  firest  14691  pwsle  14750  2oppchomf  14983  isinv  15018  invsym2  15021  invfun  15022  oppcsect2  15033  oppcinv  15034  oppchofcl  15390  oyoncl  15400  clatl  15606  gicer  16138  gsum2d2lem  16816  gsum2d2  16817  gsumcom2  16818  gsumxp  16819  gsumxpOLD  16821  dprd2d2  16907  opsrtoslem2  17960  mattpostpos  18763  mdetunilem9  18929  restbas  19465  txuni2  19893  txcls  19932  txdis1cn  19963  txkgen  19980  hmpher  20112  cnextrel  20390  tgphaus  20442  qustgplem  20446  tsmsxp  20484  utop2nei  20580  utop3cls  20581  xmeter  20763  caubl  21573  ovoliunlem1  21740  reldv  22101  taylf  22582  lgsquadlem1  23454  lgsquadlem2  23455  nvrel  25268  dfcnv2  27286  qtophaus  27599  cvmliftlem1  28481  cvmlift2lem12  28510  fprodcom2  28967  dfso2  29036  elrn3  29045  relbigcup  29400  heicant  29902  aoprssdm  31981  eliunxp2  32218  dvhopellsm  36131  dibvalrel  36177  dib1dim  36179  diclspsn  36208  dih1  36300  dih1dimatlem  36343