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

Theorem xpss 4974
Description: A cross product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
xpss  |-  ( A  X.  B )  C_  ( _V  X.  _V )

Proof of Theorem xpss
StepHypRef Expression
1 ssv 3360 . 2  |-  A  C_  _V
2 ssv 3360 . 2  |-  B  C_  _V
3 xpss12 4973 . 2  |-  ( ( A  C_  _V  /\  B  C_ 
_V )  ->  ( A  X.  B )  C_  ( _V  X.  _V )
)
41, 2, 3mp2an 654 1  |-  ( A  X.  B )  C_  ( _V  X.  _V )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2948    C_ wss 3312    X. cxp 4868
This theorem is referenced by:  relxp  4975  eqbrrdva  5034  relrelss  5385  dff3  5874  eqopi  6375  op1steq  6383  dfoprab4  6396  copsex2ga  6400  infxpenlem  7887  nqerf  8799  uzrdgfni  11290  homarel  14183  relxpchom  14270  frmdplusg  14791  upxp  17647  ustrel  18233  utop2nei  18272  utop3cls  18273  fmucndlem  18313  metustrelOLD  18577  metustrel  18578  xppreima2  24052  df1stres  24083  df2ndres  24084  metideq  24280  metider  24281  pstmfval  24283  xpinpreima2  24297  tpr2rico  24302  dya2iocnrect  24623  txprel  25716  mblfinlem  26234  dihvalrel  32014
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-opab 4259  df-xp 4876
  Copyright terms: Public domain W3C validator