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

Theorem xpss 4961
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 3490 . 2  |-  A  C_  _V
2 ssv 3490 . 2  |-  B  C_  _V
3 xpss12 4960 . 2  |-  ( ( A  C_  _V  /\  B  C_ 
_V )  ->  ( A  X.  B )  C_  ( _V  X.  _V )
)
41, 2, 3mp2an 676 1  |-  ( A  X.  B )  C_  ( _V  X.  _V )
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3087    C_ wss 3442    X. cxp 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456  df-opab 4485  df-xp 4860
This theorem is referenced by:  relxp  4962  copsex2ga  4966  eqbrrdva  5024  relrelss  5379  dff3  6050  eqopi  6841  op1steq  6849  dfoprab4  6864  infxpenlem  8443  nqerf  9354  uzrdgfni  12169  reltrclfv  13060  homarel  15873  relxpchom  16008  frmdplusg  16580  upxp  20560  ustrel  21148  utop2nei  21187  utop3cls  21188  fmucndlem  21228  metustrel  21489  xppreima2  28080  df1stres  28115  df2ndres  28116  f1od2  28143  fpwrelmap  28152  metideq  28526  metider  28527  pstmfval  28529  xpinpreima2  28543  tpr2rico  28548  esum2d  28744  dya2iocnrect  28933  mpstssv  29956  txprel  30422  bj-elid2  31376  mblfinlem1  31671  dihvalrel  34546
  Copyright terms: Public domain W3C validator