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

Theorem xpss 4792
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 3199 . 2  |-  A  C_  _V
2 ssv 3199 . 2  |-  B  C_  _V
3 xpss12 4791 . 2  |-  ( ( A  C_  _V  /\  B  C_ 
_V )  ->  ( A  X.  B )  C_  ( _V  X.  _V )
)
41, 2, 3mp2an 655 1  |-  ( A  X.  B )  C_  ( _V  X.  _V )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2789    C_ wss 3153    X. cxp 4686
This theorem is referenced by:  relxp  4793  relrelss  5194  dff3  5634  eqopi  6117  op1steq  6125  dfoprab4  6138  copsex2ga  6142  infxpenlem  7636  nqerf  8549  uzrdgfni  11015  homarel  13862  relxpchom  13949  frmdplusg  14470  upxp  17311  txprel  23827  relded  25139  relcat  25160  dihvalrel  30736
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-opab 4079  df-xp 4694
  Copyright terms: Public domain W3C validator