Theorem relxp 5681

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 (𝐴 × 𝐵)

Proof of Theorem relxp

Step	Hyp	Ref	Expression
1		xpss 5679	. 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
2		df-rel 5670	. 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
3	1, 2	mpbir 234	1 ⊢ Rel (𝐴 × 𝐵)

Syntax hints:  Vcvv 3455   ⊆ wss 3906   × cxp 5661  Rel wrel 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-opab 5175  df-xp 5669  df-rel 5670

This theorem is referenced by:  xpsspw  5798  relinxp  5803  inxp  5820  xpiindi  5823  eliunxp  5825  opeliunxp2  5826  relres  6006  restidsing  6057  codir  6122  qfto  6123  difxp  6163  sofld  6187  cnvcnv  6192  dfco2  6248  unixp  6285  ressn  6288  fliftcnv  7311  fliftfun  7312  oprssdm  7593  frxp  8123  frxp2  8141  frxp3  8148  opeliunxp2f  8207  reltpos  8228  tposfo  8250  tposf  8251  swoer  8727  xpider  8787  xpcomf1o  9055  fpwwe2lem8  10624  ordpinq  10929  addassnq  10944  mulassnq  10945  distrnq  10947  mulidnq  10949  recmulnq  10950  ltexnq  10961  prcdnq  10979  ltrel  11272  lerel  11274  dfle2  13173  fsumcom2  15827  fprodcom2  16040  0rest  17483  firest  17486  2oppchomf  17781  isinv  17818  invsym2  17821  invfun  17822  oppcsect2  17837  oppcinv  17838  oppchofcl  18317  oyoncl  18327  clatl  18565  qusxpid  19252  gicer  19348  gsum2d2lem  20044  gsum2d2  20045  gsumcom2  20046  gsumxp  20047  dprd2d2  20117  mattpostpos  22592  mdetunilem9  22758  restbas  23296  txuni2  23703  txcls  23742  txdis1cn  23773  txkgen  23790  hmpher  23922  cnextrel  24201  tgphaus  24255  qustgplem  24259  tsmsxp  24293  utop2nei  24388  utop3cls  24389  xmeter  24571  caubl  25448  ovoliunlem1  25642  reldv  26010  taylf  26505  lgsquadlem1  27525  lgsquadlem2  27526  noseqrdgfn  28480  nvrel  30935  dfcnv2  33001  gsumpart  33364  gsumwrd2dccat  33379  elrgspnsubrunlem2  33549  opprabs  33745  qtophaus  34207  cvmliftlem1  35758  cvmlift2lem12  35787  gonan0  35865  xpab  36199  dfso2  36228  relbigcup  36368  poimirlem3  38255  heicant  38287  vvdifopab  38895  cnvref4  38980  ecxrn2  39038  dvhopellsm  41872  dibvalrel  41918  dib1dim  41920  diclspsn  41949  dih1  42041  dih1dimatlem  42084  aoprssdm  47922  gricrel  48667  grlicrel  48754  eliunxp2  49097  iinxp  49592  coxp  49594  xpco2  49618  tposresxp  49644  tposf1o  49645  tposideq2  49650  joindm2  49729  meetdm2  49731  oppfvallem  49896  funcoppc3  49908  uptposlem  49958  reldmxpc  50007