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

Theorem xpss 5107
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  |-  ( A  X.  B )  C_  ( _V  X.  _V )

Proof of Theorem xpss
StepHypRef Expression
1 ssv 3524 . 2  |-  A  C_  _V
2 ssv 3524 . 2  |-  B  C_  _V
3 xpss12 5106 . 2  |-  ( ( A  C_  _V  /\  B  C_ 
_V )  ->  ( A  X.  B )  C_  ( _V  X.  _V )
)
41, 2, 3mp2an 672 1  |-  ( A  X.  B )  C_  ( _V  X.  _V )
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3113    C_ wss 3476    X. cxp 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-opab 4506  df-xp 5005
This theorem is referenced by:  relxp  5108  copsex2ga  5112  eqbrrdva  5170  relrelss  5529  dff3  6032  eqopi  6815  op1steq  6823  dfoprab4  6838  infxpenlem  8387  nqerf  9304  uzrdgfni  12032  homarel  15214  relxpchom  15301  frmdplusg  15842  upxp  19856  ustrel  20446  utop2nei  20485  utop3cls  20486  fmucndlem  20526  metustrelOLD  20790  metustrel  20791  xppreima2  27157  df1stres  27191  df2ndres  27192  f1od2  27216  fpwrelmap  27225  metideq  27505  metider  27506  pstmfval  27508  xpinpreima2  27522  tpr2rico  27527  dya2iocnrect  27889  txprel  29103  mblfinlem1  29626  bj-elid2  33673  dihvalrel  36076
  Copyright terms: Public domain W3C validator