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

Theorem xpss 5022
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 3437 . 2  |-  A  C_  _V
2 ssv 3437 . 2  |-  B  C_  _V
3 xpss12 5021 . 2  |-  ( ( A  C_  _V  /\  B  C_ 
_V )  ->  ( A  X.  B )  C_  ( _V  X.  _V )
)
41, 2, 3mp2an 670 1  |-  ( A  X.  B )  C_  ( _V  X.  _V )
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3034    C_ wss 3389    X. cxp 4911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396  df-ss 3403  df-opab 4426  df-xp 4919
This theorem is referenced by:  relxp  5023  copsex2ga  5027  eqbrrdva  5085  relrelss  5439  dff3  5946  eqopi  6733  op1steq  6741  dfoprab4  6756  infxpenlem  8304  nqerf  9219  uzrdgfni  11972  reltrclfv  12855  homarel  15432  relxpchom  15567  frmdplusg  16139  upxp  20209  ustrel  20799  utop2nei  20838  utop3cls  20839  fmucndlem  20879  metustrelOLD  21143  metustrel  21144  xppreima2  27628  df1stres  27669  df2ndres  27670  f1od2  27697  fpwrelmap  27706  metideq  28026  metider  28027  pstmfval  28029  xpinpreima2  28043  tpr2rico  28048  esum2d  28241  dya2iocnrect  28408  mpstssv  29088  txprel  29682  mblfinlem1  30216  bj-elid2  34948  dihvalrel  37419
  Copyright terms: Public domain W3C validator