Theorem relxp 5575

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 5573	. 2 ⊢ (𝐴 × 𝐵) ⊆ (V × V)
2		df-rel 5564	. 2 ⊢ (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
3	1, 2	mpbir 233	1 ⊢ Rel (𝐴 × 𝐵)

Syntax hints:  Vcvv 3496   ⊆ wss 3938   × cxp 5555  Rel wrel 5562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-opab 5131  df-xp 5563  df-rel 5564

This theorem is referenced by:  xpsspw  5684  relinxp  5689  xpiindi  5708  eliunxp  5710  opeliunxp2  5711  relres  5884  restidsing  5924  codir  5982  qfto  5983  difxp  6023  sofld  6046  cnvcnv  6051  dfco2  6100  unixp  6135  ressn  6138  fliftcnv  7066  fliftfun  7067  oprssdm  7331  frxp  7822  opeliunxp2f  7878  reltpos  7899  tposfo  7921  tposf  7922  swoer  8321  xpider  8370  xpcomf1o  8608  fpwwe2lem9  10062  ordpinq  10367  addassnq  10382  mulassnq  10383  distrnq  10385  mulidnq  10387  recmulnq  10388  ltexnq  10399  prcdnq  10417  ltrel  10705  lerel  10707  dfle2  12543  fsumcom2  15131  fprodcom2  15340  0rest  16705  firest  16708  2oppchomf  16996  isinv  17032  invsym2  17035  invfun  17036  oppcsect2  17051  oppcinv  17052  oppchofcl  17512  oyoncl  17522  clatl  17728  gicer  18418  gsum2d2lem  19095  gsum2d2  19096  gsumcom2  19097  gsumxp  19098  dprd2d2  19168  mattpostpos  21065  mdetunilem9  21231  restbas  21768  txuni2  22175  txcls  22214  txdis1cn  22245  txkgen  22262  hmpher  22394  cnextrel  22673  tgphaus  22727  qustgplem  22731  tsmsxp  22765  utop2nei  22861  utop3cls  22862  xmeter  23045  caubl  23913  ovoliunlem1  24105  reldv  24470  taylf  24951  lgsquadlem1  25958  lgsquadlem2  25959  nvrel  28381  dfcnv2  30424  qusxpid  30930  qtophaus  31102  cvmliftlem1  32534  cvmlift2lem12  32563  gonan0  32641  dfso2  32992  relbigcup  33360  poimirlem3  34897  heicant  34929  vvdifopab  35523  dvhopellsm  38255  dibvalrel  38301  dib1dim  38303  diclspsn  38332  dih1  38424  dih1dimatlem  38467  aoprssdm  43408  eliunxp2  44389