Theorem relxp 5598

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

Syntax hints:  Vcvv 3422   ⊆ wss 3883   × cxp 5578  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587

This theorem is referenced by:  xpsspw  5708  relinxp  5713  xpiindi  5733  eliunxp  5735  opeliunxp2  5736  relres  5909  restidsing  5951  codir  6014  qfto  6015  difxp  6056  sofld  6079  cnvcnv  6084  dfco2  6138  unixp  6174  ressn  6177  fliftcnv  7162  fliftfun  7163  oprssdm  7431  frxp  7938  opeliunxp2f  7997  reltpos  8018  tposfo  8040  tposf  8041  swoer  8486  xpider  8535  xpcomf1o  8801  fpwwe2lem8  10325  ordpinq  10630  addassnq  10645  mulassnq  10646  distrnq  10648  mulidnq  10650  recmulnq  10651  ltexnq  10662  prcdnq  10680  ltrel  10968  lerel  10970  dfle2  12810  fsumcom2  15414  fprodcom2  15622  0rest  17057  firest  17060  2oppchomf  17352  isinv  17389  invsym2  17392  invfun  17393  oppcsect2  17408  oppcinv  17409  oppchofcl  17894  oyoncl  17904  clatl  18141  gicer  18807  gsum2d2lem  19489  gsum2d2  19490  gsumcom2  19491  gsumxp  19492  dprd2d2  19562  mattpostpos  21511  mdetunilem9  21677  restbas  22217  txuni2  22624  txcls  22663  txdis1cn  22694  txkgen  22711  hmpher  22843  cnextrel  23122  tgphaus  23176  qustgplem  23180  tsmsxp  23214  utop2nei  23310  utop3cls  23311  xmeter  23494  caubl  24377  ovoliunlem1  24571  reldv  24939  taylf  25425  lgsquadlem1  26433  lgsquadlem2  26434  nvrel  28865  dfcnv2  30915  gsumpart  31217  qusxpid  31461  qtophaus  31688  cvmliftlem1  33147  cvmlift2lem12  33176  gonan0  33254  xpab  33579  dfso2  33628  frxp2  33718  frxp3  33724  relbigcup  34126  poimirlem3  35707  heicant  35739  vvdifopab  36326  dvhopellsm  39058  dibvalrel  39104  dib1dim  39106  diclspsn  39135  dih1  39227  dih1dimatlem  39270  aoprssdm  44581  eliunxp2  45557  joindm2  46150  meetdm2  46152