Theorem relxp 4920

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 4919	. 2 |- ( A X. B ) C_ ( _V X. _V )
2		df-rel 4819	. 2 |- ( Rel ( A X. B ) <-> ( A X. B ) C_ ( _V X. _V ) )
3	1, 2	mpbir 214	1 |- Rel ( A X. B )

Syntax hints:   _Vcvv 3013   C_ wss 3372   X. cxp 4810   Rel wrel 4817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-in 3379  df-ss 3386  df-opab 4434  df-xp 4818  df-rel 4819

This theorem is referenced by:  xpsspw  4926  xpiindi  4948  eliunxp  4950  opeliunxp2  4951  relres  5110  restidsing  5139  codir  5198  qfto  5199  difxp  5239  sofld  5262  cnvcnv  5267  dfco2  5313  unixp  5348  ressn  5351  fliftcnv  6190  fliftfun  6191  oprssdm  6438  frxp  6894  opeliunxp2f  6944  reltpos  6965  tpostpos  6980  tposfo  6987  tposf  6988  swoer  7378  xpider  7421  erinxp  7424  xpcomf1o  7648  cda1dif  8593  brdom3  8943  brdom5  8944  brdom4  8945  fpwwe2lem8  9049  fpwwe2lem9  9050  fpwwe2lem12  9053  ordpinq  9355  addassnq  9370  mulassnq  9371  distrnq  9373  mulidnq  9375  recmulnq  9376  ltexnq  9387  prcdnq  9405  ltrel  9683  lerel  9685  dfle2  11436  fsumcom2  13846  fprodcom2  14049  0rest  15339  firest  15342  pwsle  15401  2oppchomf  15640  isinv  15676  invsym2  15679  invfun  15680  oppcsect2  15695  oppcinv  15696  oppchofcl  16156  oyoncl  16166  clatl  16373  gicer  16951  gsum2d2lem  17616  gsum2d2  17617  gsumcom2  17618  gsumxp  17619  dprd2d2  17688  opsrtoslem2  18719  mattpostpos  19490  mdetunilem9  19656  restbas  20185  txuni2  20591  txcls  20630  txdis1cn  20661  txkgen  20678  hmpher  20810  cnextrel  21089  tgphaus  21142  qustgplem  21146  tsmsxp  21180  utop2nei  21276  utop3cls  21277  xmeter  21459  caubl  22288  ovoliunlem1  22466  reldv  22837  taylf  23328  lgsquadlem1  24294  lgsquadlem2  24295  nvrel  26233  dfcnv2  28287  qtophaus  28670  cvmliftlem1  30014  cvmlift2lem12  30043  dfso2  30400  elrn3  30409  relbigcup  30670  poimirlem3  31945  heicant  31977  dvhopellsm  34687  dibvalrel  34733  dib1dim  34735  diclspsn  34764  dih1  34856  dih1dimatlem  34899  aoprssdm  38795  eliunxp2  40440