Theorem relxp 5036

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 5035	. 2 |- ( A X. B ) C_ ( _V X. _V )
2		df-rel 4933	. 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 3047   C_ wss 3402   X. cxp 4924   Rel wrel 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-v 3049  df-in 3409  df-ss 3416  df-opab 4439  df-xp 4932  df-rel 4933

This theorem is referenced by:  xpsspw  5042  xpiindi  5064  eliunxp  5066  opeliunxp2  5067  relres  5226  restidsing  5255  codir  5313  qfto  5314  difxp  5354  sofld  5377  cnvcnv  5381  dfco2  5427  unixp  5462  ressn  5465  fliftcnv  6128  fliftfun  6129  oprssdm  6373  frxp  6827  reltpos  6896  tpostpos  6911  tposfo  6918  tposf  6919  swoer  7275  xpider  7318  erinxp  7321  xpcomf1o  7543  cda1dif  8487  brdom3  8837  brdom5  8838  brdom4  8839  fpwwe2lem8  8944  fpwwe2lem9  8945  fpwwe2lem12  8948  ordpinq  9250  addassnq  9265  mulassnq  9266  distrnq  9268  mulidnq  9270  recmulnq  9271  ltexnq  9282  prcdnq  9300  ltrel  9578  lerel  9580  dfle2  11292  fsumcom2  13610  fprodcom2  13809  0rest  14856  firest  14859  pwsle  14918  2oppchomf  15149  isinv  15185  invsym2  15188  invfun  15189  oppcsect2  15204  oppcinv  15205  oppchofcl  15665  oyoncl  15675  clatl  15882  gicer  16460  gsum2d2lem  17134  gsum2d2  17135  gsumcom2  17136  gsumxp  17137  dprd2d2  17225  opsrtoslem2  18281  mattpostpos  19060  mdetunilem9  19226  restbas  19764  txuni2  20170  txcls  20209  txdis1cn  20240  txkgen  20257  hmpher  20389  cnextrel  20667  tgphaus  20719  qustgplem  20723  tsmsxp  20761  utop2nei  20857  utop3cls  20858  xmeter  21040  caubl  21850  ovoliunlem1  22017  reldv  22378  taylf  22860  lgsquadlem1  23765  lgsquadlem2  23766  nvrel  25633  dfcnv2  27694  qtophaus  28024  cvmliftlem1  28955  cvmlift2lem12  28984  dfso2  29385  elrn3  29394  relbigcup  29736  heicant  30250  aoprssdm  32488  eliunxp2  33158  dvhopellsm  37292  dibvalrel  37338  dib1dim  37340  diclspsn  37369  dih1  37461  dih1dimatlem  37504