Theorem relxp 5096

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 5095	. 2 |- ( A X. B ) C_ ( _V X. _V )
2		df-rel 4992	. 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 3093   C_ wss 3458   X. cxp 4983   Rel wrel 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465  df-ss 3472  df-opab 4492  df-xp 4991  df-rel 4992

This theorem is referenced by:  xpsspwOLD  5103  xpiindi  5124  eliunxp  5126  opeliunxp2  5127  relres  5287  restidsing  5316  codir  5373  qfto  5374  difxp  5417  sofld  5441  cnvcnv  5445  dfco2  5492  unixp  5526  ressn  5529  fliftcnv  6190  fliftfun  6191  oprssdm  6437  frxp  6891  reltpos  6958  tpostpos  6973  tposfo  6980  tposf  6981  swoer  7337  xpider  7380  erinxp  7383  xpcomf1o  7604  cda1dif  8554  brdom3  8904  brdom5  8905  brdom4  8906  fpwwe2lem8  9013  fpwwe2lem9  9014  fpwwe2lem12  9017  ordpinq  9319  addassnq  9334  mulassnq  9335  distrnq  9337  mulidnq  9339  recmulnq  9340  ltexnq  9351  prcdnq  9369  ltrel  9647  lerel  9649  dfle2  11357  fsumcom2  13563  0rest  14699  firest  14702  pwsle  14761  2oppchomf  14991  isinv  15026  invsym2  15029  invfun  15030  oppcsect2  15041  oppcinv  15042  oppchofcl  15398  oyoncl  15408  clatl  15615  gicer  16193  gsum2d2lem  16870  gsum2d2  16871  gsumcom2  16872  gsumxp  16873  gsumxpOLD  16875  dprd2d2  16961  opsrtoslem2  18017  mattpostpos  18823  mdetunilem9  18989  restbas  19525  txuni2  19932  txcls  19971  txdis1cn  20002  txkgen  20019  hmpher  20151  cnextrel  20429  tgphaus  20481  qustgplem  20485  tsmsxp  20523  utop2nei  20619  utop3cls  20620  xmeter  20802  caubl  21612  ovoliunlem1  21779  reldv  22140  taylf  22621  lgsquadlem1  23494  lgsquadlem2  23495  nvrel  25360  dfcnv2  27382  qtophaus  27705  cvmliftlem1  28596  cvmlift2lem12  28625  fprodcom2  29082  dfso2  29151  elrn3  29160  relbigcup  29515  heicant  30017  aoprssdm  32121  eliunxp2  32631  dvhopellsm  36546  dibvalrel  36592  dib1dim  36594  diclspsn  36623  dih1  36715  dih1dimatlem  36758