Theorem relxp 4961

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

Syntax hints:   _Vcvv 3080   C_ wss 3436   X. cxp 4851   Rel wrel 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443  df-ss 3450  df-opab 4483  df-xp 4859  df-rel 4860

This theorem is referenced by:  xpsspw  4967  xpiindi  4989  eliunxp  4991  opeliunxp2  4992  relres  5151  restidsing  5180  codir  5239  qfto  5240  difxp  5280  sofld  5303  cnvcnv  5307  dfco2  5353  unixp  5388  ressn  5391  fliftcnv  6219  fliftfun  6220  oprssdm  6464  frxp  6917  opeliunxp2f  6967  reltpos  6989  tpostpos  7004  tposfo  7011  tposf  7012  swoer  7402  xpider  7445  erinxp  7448  xpcomf1o  7670  cda1dif  8613  brdom3  8963  brdom5  8964  brdom4  8965  fpwwe2lem8  9069  fpwwe2lem9  9070  fpwwe2lem12  9073  ordpinq  9375  addassnq  9390  mulassnq  9391  distrnq  9393  mulidnq  9395  recmulnq  9396  ltexnq  9407  prcdnq  9425  ltrel  9703  lerel  9705  dfle2  11453  fsumcom2  13834  fprodcom2  14037  0rest  15327  firest  15330  pwsle  15389  2oppchomf  15628  isinv  15664  invsym2  15667  invfun  15668  oppcsect2  15683  oppcinv  15684  oppchofcl  16144  oyoncl  16154  clatl  16361  gicer  16939  gsum2d2lem  17604  gsum2d2  17605  gsumcom2  17606  gsumxp  17607  dprd2d2  17676  opsrtoslem2  18707  mattpostpos  19477  mdetunilem9  19643  restbas  20172  txuni2  20578  txcls  20617  txdis1cn  20648  txkgen  20665  hmpher  20797  cnextrel  21076  tgphaus  21129  qustgplem  21133  tsmsxp  21167  utop2nei  21263  utop3cls  21264  xmeter  21446  caubl  22275  ovoliunlem1  22453  reldv  22823  taylf  23314  lgsquadlem1  24280  lgsquadlem2  24281  nvrel  26219  dfcnv2  28281  qtophaus  28671  cvmliftlem1  30016  cvmlift2lem12  30045  dfso2  30401  elrn3  30410  relbigcup  30669  poimirlem3  31907  heicant  31939  dvhopellsm  34654  dibvalrel  34700  dib1dim  34702  diclspsn  34731  dih1  34823  dih1dimatlem  34866  aoprssdm  38574  eliunxp2  39736