Theorem relxp 5217

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

Syntax hints:  Vcvv 3195   ⊆ wss 3567   × cxp 5102  Rel wrel 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581  df-opab 4704  df-xp 5110  df-rel 5111

This theorem is referenced by:  xpsspw  5223  xpiindi  5246  eliunxp  5248  opeliunxp2  5249  relres  5414  restidsing  5446  restidsingOLD  5447  codir  5504  qfto  5505  difxp  5546  sofld  5569  cnvcnv  5574  cnvcnvOLD  5575  dfco2  5622  unixp  5656  ressn  5659  fliftcnv  6546  fliftfun  6547  oprssdm  6800  frxp  7272  opeliunxp2f  7321  reltpos  7342  tpostpos  7357  tposfo  7364  tposf  7365  swoer  7757  xpider  7803  erinxp  7806  xpcomf1o  8034  cda1dif  8983  brdom3  9335  brdom5  9336  brdom4  9337  fpwwe2lem8  9444  fpwwe2lem9  9445  fpwwe2lem12  9448  ordpinq  9750  addassnq  9765  mulassnq  9766  distrnq  9768  mulidnq  9770  recmulnq  9771  ltexnq  9782  prcdnq  9800  ltrel  10085  lerel  10087  dfle2  11965  fsumcom2  14486  fsumcom2OLD  14487  fprodcom2  14695  fprodcom2OLD  14696  0rest  16071  firest  16074  pwsle  16133  2oppchomf  16365  isinv  16401  invsym2  16404  invfun  16405  oppcsect2  16420  oppcinv  16421  oppchofcl  16881  oyoncl  16891  clatl  17097  gicer  17699  gicerOLD  17700  gsum2d2lem  18353  gsum2d2  18354  gsumcom2  18355  gsumxp  18356  dprd2d2  18424  opsrtoslem2  19466  mattpostpos  20241  mdetunilem9  20407  restbas  20943  txuni2  21349  txcls  21388  txdis1cn  21419  txkgen  21436  hmpher  21568  cnextrel  21848  tgphaus  21901  qustgplem  21905  tsmsxp  21939  utop2nei  22035  utop3cls  22036  xmeter  22219  caubl  23087  ovoliunlem1  23251  reldv  23615  taylf  24096  lgsquadlem1  25086  lgsquadlem2  25087  nvrel  27427  dfcnv2  29450  qtophaus  29877  cvmliftlem1  31241  cvmlift2lem12  31270  dfso2  31619  elrn3  31628  relbigcup  31979  poimirlem3  33383  heicant  33415  dvhopellsm  36225  dibvalrel  36271  dib1dim  36273  diclspsn  36302  dih1  36394  dih1dimatlem  36437  aoprssdm  41045  eliunxp2  41877