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

Theorem xpss 5135
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 3584 . 2 𝐴 ⊆ V
2 ssv 3584 . 2 𝐵 ⊆ V
3 xpss12 5134 . 2 ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V))
41, 2, 3mp2an 703 1 (𝐴 × 𝐵) ⊆ (V × V)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3169  wss 3536   × cxp 5023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-in 3543  df-ss 3550  df-opab 4635  df-xp 5031
This theorem is referenced by:  relxp  5136  copsex2ga  5140  eqbrrdva  5198  relrelss  5559  dff3  6262  eqopi  7067  op1steq  7075  dfoprab4  7090  infxpenlem  8693  nqerf  9605  uzrdgfni  12571  reltrclfv  13549  homarel  16452  relxpchom  16587  frmdplusg  17157  upxp  21175  ustrel  21764  utop2nei  21803  utop3cls  21804  fmucndlem  21844  metustrel  22105  xppreima2  28633  df1stres  28667  df2ndres  28668  f1od2  28690  fpwrelmap  28699  metideq  29067  metider  29068  pstmfval  29070  xpinpreima2  29084  tpr2rico  29089  esum2d  29285  dya2iocnrect  29473  mpstssv  30493  txprel  30959  bj-elid2  32063  elxp8  32195  mblfinlem1  32416  dihvalrel  35386  rfovcnvf1od  37118  ovolval2lem  39334
  Copyright terms: Public domain W3C validator