MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpss Structured version   Visualization version   GIF version

Theorem xpss 5701
Description: A Cartesian product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
xpss (𝐴 × 𝐵) ⊆ (V × V)

Proof of Theorem xpss
StepHypRef Expression
1 ssv 4008 . 2 𝐴 ⊆ V
2 ssv 4008 . 2 𝐵 ⊆ V
3 xpss12 5700 . 2 ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V))
41, 2, 3mp2an 692 1 (𝐴 × 𝐵) ⊆ (V × V)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3480  wss 3951   × cxp 5683
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691
This theorem is referenced by:  relxp  5703  copsex2ga  5817  eqbrrdva  5880  relrelss  6293  dff3  7120  eqopi  8050  op1steq  8058  dfoprab4  8080  infxpenlem  10053  nqerf  10970  uzrdgfni  13999  reltrclfv  15056  homarel  18081  relxpchom  18226  frmdplusg  18867  psdmul  22170  upxp  23631  ustrel  24220  utop2nei  24259  utop3cls  24260  fmucndlem  24300  metustrel  24565  xppreima2  32661  df1stres  32713  df2ndres  32714  f1od2  32732  fsuppcurry1  32736  fsuppcurry2  32737  fpwrelmap  32744  metideq  33892  metider  33893  pstmfval  33895  xpinpreima2  33906  tpr2rico  33911  esum2d  34094  dya2iocnrect  34283  mpstssv  35544  txprel  35880  elxp8  37372  mblfinlem1  37664  xrnrel  38374  dihvalrel  41281  rfovcnvf1od  44017  ovolval2lem  46658  sprsymrelfo  47484
  Copyright terms: Public domain W3C validator