Theorem relxp 5684

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

This proof depends on syntax axioms:  Vcvv 3458   ⊆ wss 3908   × cxp 5664  Rel wrel 5671

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-opab 5179  df-xp 5672  df-rel 5673

This theorem is used by:  xpsspw  5801  relinxp  5806  inxp  5823  xpiindi  5826  eliunxp  5828  opeliunxp2  5829  relres  6009  restidsing  6060  codir  6125  qfto  6126  difxp  6166  sofld  6190  cnvcnv  6195  dfco2  6251  unixp  6290  ressn  6293  fliftcnv  7320  fliftfun  7321  oprssdm  7604  frxp  8131  frxp2  8149  frxp3  8156  opeliunxp2f  8215  reltpos  8236  tposfo  8258  tposf  8259  swoer  8735  xpider  8795  xpcomf1o  9064  fpwwe2lem8  10641  ordpinq  10946  addassnq  10961  mulassnq  10962  distrnq  10964  mulidnq  10966  recmulnq  10967  ltexnq  10978  prcdnq  10996  ltrel  11289  lerel  11291  dfle2  13190  fsumcom2  15851  fprodcom2  16064  0rest  17507  firest  17510  2oppchomf  17805  isinv  17842  invsym2  17845  invfun  17846  oppcsect2  17861  oppcinv  17862  oppchofcl  18341  oyoncl  18351  clatl  18589  qusxpid  19282  gicer  19378  gsum2d2lem  20074  gsum2d2  20075  gsumcom2  20076  gsumxp  20077  dprd2d2  20147  ricrel  20629  mattpostpos  22648  mdetunilem9  22814  restbas  23352  txuni2  23759  txcls  23798  txdis1cn  23829  txkgen  23846  hmpher  23978  cnextrel  24257  tgphaus  24311  qustgplem  24315  tsmsxp  24349  utop2nei  24444  utop3cls  24445  xmeter  24627  caubl  25504  ovoliunlem1  25698  reldv  26066  taylf  26561  lgsquadlem1  27581  lgsquadlem2  27582  noseqrdgfn  28536  nvrel  30991  dfcnv2  33057  gsumpart  33414  gsumwrd2dccat  33429  elrgspnsubrunlem2  33599  opprabs  33795  qtophaus  34257  cvmliftlem1  35798  cvmlift2lem12  35827  gonan0  35905  xpab  36239  dfso2  36268  relbigcup  36408  poimirlem3  38315  heicant  38347  vvdifopab  38955  cnvref4  39040  ecxrn2  39098  dvhopellsm  41932  dibvalrel  41978  dib1dim  41980  diclspsn  42009  dih1  42101  dih1dimatlem  42144  aoprssdm  47980  gricrel  48725  grlicrel  48812  eliunxp2  49155  iinxp  49650  coxp  49652  xpco2  49676  tposresxp  49702  tposf1o  49703  tposideq2  49708  joindm2  49787  meetdm2  49789  oppfvallem  49954  funcoppc3  49966  uptposlem  50016  reldmxpc  50065