Theorem relxp 4968

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 4967	. 2 |- ( A X. B ) C_ ( _V X. _V )
2		df-rel 4868	. 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 2993   C_ wss 3349   X. cxp 4859   Rel wrel 4866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363  df-opab 4372  df-xp 4867  df-rel 4868

This theorem is referenced by:  xpsspwOLD  4975  xpiindi  4996  eliunxp  4998  opeliunxp2  4999  relres  5159  restidsing  5183  codir  5239  qfto  5240  difxp  5283  sofld  5307  cnvcnv  5311  dfco2  5358  unixp  5391  ressn  5394  fliftcnv  6025  fliftfun  6026  oprssdm  6265  frxp  6703  reltpos  6771  tpostpos  6786  tposfo  6793  tposf  6794  swoer  7150  xpider  7192  erinxp  7195  xpcomf1o  7421  cda1dif  8366  brdom3  8716  brdom5  8717  brdom4  8718  fpwwe2lem8  8825  fpwwe2lem9  8826  fpwwe2lem12  8829  ordpinq  9133  addassnq  9148  mulassnq  9149  distrnq  9151  mulidnq  9153  recmulnq  9154  ltexnq  9165  prcdnq  9183  ltrel  9460  lerel  9462  dfle2  11145  fsumcom2  13262  0rest  14389  firest  14392  pwsle  14451  2oppchomf  14684  isinv  14719  invsym2  14722  invfun  14723  oppcsect2  14734  oppcinv  14735  oppchofcl  15091  oyoncl  15101  clatl  15307  gicer  15825  gsum2d2lem  16487  gsum2d2  16488  gsumcom2  16489  gsumxp  16490  gsumxpOLD  16492  dprd2d2  16565  opsrtoslem2  17588  mattpostpos  18360  mdetunilem9  18448  restbas  18784  txuni2  19160  txcls  19199  txdis1cn  19230  txkgen  19247  hmpher  19379  cnextrel  19657  tgphaus  19709  divstgplem  19713  tsmsxp  19751  utop2nei  19847  utop3cls  19848  xmeter  20030  caubl  20840  ovoliunlem1  21007  reldv  21367  taylf  21848  lgsquadlem1  22715  lgsquadlem2  22716  nvrel  24002  dfcnv2  26016  cvmliftlem1  27196  cvmlift2lem12  27225  fprodcom2  27517  dfso2  27586  elrn3  27595  relbigcup  27950  heicant  28452  aoprssdm  30134  eliunxp2  30747  dvhopellsm  34858  dibvalrel  34904  dib1dim  34906  diclspsn  34935  dih1  35027  dih1dimatlem  35070