Theorem relxp 5661

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

Syntax hints:  Vcvv 3453   ⊆ wss 3902   × cxp 5641  Rel wrel 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-opab 5160  df-xp 5649  df-rel 5650

This theorem is referenced by:  xpsspw  5778  relinxp  5783  inxp  5800  xpiindi  5803  eliunxp  5805  opeliunxp2  5806  relres  5987  restidsing  6037  codir  6102  qfto  6103  difxp  6144  sofld  6167  cnvcnv  6172  dfco2  6226  unixp  6263  ressn  6266  fliftcnv  7289  fliftfun  7290  oprssdm  7571  frxp  8099  frxp2  8117  frxp3  8124  opeliunxp2f  8183  reltpos  8204  tposfo  8226  tposf  8227  swoer  8703  xpider  8763  xpcomf1o  9031  fpwwe2lem8  10589  ordpinq  10894  addassnq  10909  mulassnq  10910  distrnq  10912  mulidnq  10914  recmulnq  10915  ltexnq  10926  prcdnq  10944  ltrel  11237  lerel  11239  dfle2  13142  fsumcom2  15791  fprodcom2  16004  0rest  17448  firest  17451  2oppchomf  17746  isinv  17783  invsym2  17786  invfun  17787  oppcsect2  17802  oppcinv  17803  oppchofcl  18282  oyoncl  18292  clatl  18530  gicer  19307  gsum2d2lem  20003  gsum2d2  20004  gsumcom2  20005  gsumxp  20006  dprd2d2  20076  mattpostpos  22501  mdetunilem9  22667  restbas  23205  txuni2  23612  txcls  23651  txdis1cn  23682  txkgen  23699  hmpher  23831  cnextrel  24110  tgphaus  24164  qustgplem  24168  tsmsxp  24202  utop2nei  24297  utop3cls  24298  xmeter  24480  caubl  25357  ovoliunlem1  25551  reldv  25919  taylf  26411  lgsquadlem1  27431  lgsquadlem2  27432  noseqrdgfn  28386  nvrel  30761  dfcnv2  32837  gsumpart  33203  gsumwrd2dccat  33218  elrgspnsubrunlem2  33389  qusxpid  33509  opprabs  33630  qtophaus  34093  cvmliftlem1  35595  cvmlift2lem12  35624  gonan0  35702  xpab  36036  dfso2  36065  relbigcup  36205  poimirlem3  38082  heicant  38114  vvdifopab  38724  cnvref4  38809  ecxrn2  38867  dvhopellsm  41701  dibvalrel  41747  dib1dim  41749  diclspsn  41778  dih1  41870  dih1dimatlem  41913  aoprssdm  47756  gricrel  48501  grlicrel  48588  eliunxp2  48916  iinxp  49412  coxp  49414  xpco2  49438  tposresxp  49464  tposf1o  49465  tposideq2  49470  joindm2  49549  meetdm2  49551  oppfvallem  49716  funcoppc3  49728  uptposlem  49778  reldmxpc  49827