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

Theorem xpss 5197
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 3610 . 2 𝐴 ⊆ V
2 ssv 3610 . 2 𝐵 ⊆ V
3 xpss12 5196 . 2 ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V))
41, 2, 3mp2an 707 1 (𝐴 × 𝐵) ⊆ (V × V)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3190  wss 3560   × cxp 5082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-in 3567  df-ss 3574  df-opab 4684  df-xp 5090
This theorem is referenced by:  relxp  5198  copsex2ga  5202  eqbrrdva  5261  relrelss  5628  dff3  6338  eqopi  7162  op1steq  7170  dfoprab4  7185  infxpenlem  8796  nqerf  9712  uzrdgfni  12713  reltrclfv  13708  homarel  16626  relxpchom  16761  frmdplusg  17331  upxp  21366  ustrel  21955  utop2nei  21994  utop3cls  21995  fmucndlem  22035  metustrel  22297  xppreima2  29333  df1stres  29365  df2ndres  29366  f1od2  29383  fpwrelmap  29392  metideq  29760  metider  29761  pstmfval  29763  xpinpreima2  29777  tpr2rico  29782  esum2d  29978  dya2iocnrect  30166  mpstssv  31197  txprel  31681  bj-elid2  32758  elxp8  32890  mblfinlem1  33117  dihvalrel  36087  rfovcnvf1od  37819  ovolval2lem  40194  sprsymrelfo  41065
  Copyright terms: Public domain W3C validator