Theorem relxp 5656

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

Syntax hints:  Vcvv 3447   ⊆ wss 3914   × cxp 5636  Rel wrel 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  xpsspw  5772  relinxp  5777  inxp  5795  xpiindi  5799  eliunxp  5801  opeliunxp2  5802  relres  5976  restidsing  6024  codir  6093  qfto  6094  difxp  6137  sofld  6160  cnvcnv  6165  dfco2  6218  unixp  6255  ressn  6258  fliftcnv  7286  fliftfun  7287  oprssdm  7570  frxp  8105  frxp2  8123  frxp3  8130  opeliunxp2f  8189  reltpos  8210  tposfo  8232  tposf  8233  swoer  8702  xpider  8761  xpcomf1o  9030  fpwwe2lem8  10591  ordpinq  10896  addassnq  10911  mulassnq  10912  distrnq  10914  mulidnq  10916  recmulnq  10917  ltexnq  10928  prcdnq  10946  ltrel  11236  lerel  11238  dfle2  13107  fsumcom2  15740  fprodcom2  15950  0rest  17392  firest  17395  2oppchomf  17685  isinv  17722  invsym2  17725  invfun  17726  oppcsect2  17741  oppcinv  17742  oppchofcl  18221  oyoncl  18231  clatl  18467  gicer  19209  gsum2d2lem  19903  gsum2d2  19904  gsumcom2  19905  gsumxp  19906  dprd2d2  19976  mattpostpos  22341  mdetunilem9  22507  restbas  23045  txuni2  23452  txcls  23491  txdis1cn  23522  txkgen  23539  hmpher  23671  cnextrel  23950  tgphaus  24004  qustgplem  24008  tsmsxp  24042  utop2nei  24138  utop3cls  24139  xmeter  24321  caubl  25208  ovoliunlem1  25403  reldv  25771  taylf  26268  lgsquadlem1  27291  lgsquadlem2  27292  noseqrdgfn  28200  nvrel  30531  dfcnv2  32600  gsumpart  32997  gsumwrd2dccat  33007  elrgspnsubrunlem2  33199  qusxpid  33334  opprabs  33453  qtophaus  33826  cvmliftlem1  35272  cvmlift2lem12  35301  gonan0  35379  xpab  35713  dfso2  35742  relbigcup  35885  poimirlem3  37617  heicant  37649  vvdifopab  38249  cnvref4  38332  dvhopellsm  41111  dibvalrel  41157  dib1dim  41159  diclspsn  41188  dih1  41280  dih1dimatlem  41323  aoprssdm  47203  gricrel  47919  grlicrel  47998  eliunxp2  48322  iinxp  48819  coxp  48821  xpco2  48845  tposresxp  48871  tposf1o  48872  tposideq2  48877  joindm2  48956  meetdm2  48958  oppfvallem  49124  funcoppc3  49136  uptposlem  49186  reldmxpc  49235