Theorem relxp 5668

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

This proof depends on syntax axioms:  Vcvv 3450   ⊆ wss 3895   × cxp 5648  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  xpsspw  5786  relinxp  5791  inxp  5808  xpiindi  5811  eliunxp  5813  opeliunxp2  5814  relres  5995  restidsing  6044  codir  6113  qfto  6114  cnvxp  6146  difxp  6154  sofld  6178  cnvcnv  6183  dfco2  6246  unixp  6285  ressn  6288  fliftcnv  7320  fliftfun  7321  oprssdm  7603  frxp  8141  frxp2  8164  frxp3  8171  opeliunxp2f  8231  reltpos  8252  tposfo  8274  tposf  8275  swoer  8753  xpider  8813  xpcomf1o  9089  fpwwe2lem8  10727  ordpinq  11032  addassnq  11047  mulassnq  11048  distrnq  11050  mulidnq  11052  recmulnq  11053  ltexnq  11064  prcdnq  11082  ltrel  11375  lerel  11377  dfle2  13280  fsumcom2  15946  fprodcom2  16157  0rest  17606  firest  17609  2oppchomf  17904  isinv  17941  invsym2  17944  invfun  17945  oppcsect2  17960  oppcinv  17961  oppchofcl  18440  oyoncl  18450  clatl  18688  qusxpid  19401  gicer  19497  gsum2d2lem  20193  gsum2d2  20194  gsumcom2  20195  gsumxp  20196  dprd2d2  20266  ricrel  20750  mattpostpos  22775  mdetunilem9  22941  restbas  23482  txuni2  23890  txcls  23929  txdis1cn  23960  txkgen  23977  hmpher  24109  cnextrel  24388  tgphaus  24442  qustgplem  24446  tsmsxp  24480  utop2nei  24575  utop3cls  24576  xmeter  24758  caubl  25635  ovoliunlem1  25829  reldv  26196  taylf  26694  lgsquadlem1  27713  lgsquadlem2  27714  noseqrdgfn  28698  nvrel  31210  dfcnv2  33317  gsumpart  33671  gsumwrd2dccat  33686  elrgspnsubrunlem2  33856  opprabs  34053  qtophaus  34515  cvmliftlem1  36137  cvmlift2lem12  36166  gonan0  36244  xpab  36584  dfso2  36613  relbigcup  36752  poimirlem3  38635  heicant  38667  vvdifopab  39291  cnvref4  39376  ecxrn2  39434  dvhopellsm  42268  dibvalrel  42314  dib1dim  42316  diclspsn  42345  dih1  42437  dih1dimatlem  42480  hfstructfun  46120  aoprssdm  48366  gricrel  49111  grlicrel  49198  eliunxp2  49540  iinxp  50036  coxp  50038  xpco2  50062  tposresxp  50090  tposf1o  50091  tposideq2  50096  joindm2  50176  meetdm2  50178  oppfvallem  50345  funcoppc3  50357  uptposlem  50407  reldmxpc  50462