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

Theorem xpss 4951
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 3381 . 2  |-  A  C_  _V
2 ssv 3381 . 2  |-  B  C_  _V
3 xpss12 4950 . 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 2977    C_ wss 3333    X. cxp 4843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340  df-ss 3347  df-opab 4356  df-xp 4851
This theorem is referenced by:  relxp  4952  copsex2ga  4956  eqbrrdva  5014  relrelss  5366  dff3  5861  eqopi  6615  op1steq  6623  dfoprab4  6636  infxpenlem  8185  nqerf  9104  uzrdgfni  11786  homarel  14909  relxpchom  14996  frmdplusg  15537  upxp  19201  ustrel  19791  utop2nei  19830  utop3cls  19831  fmucndlem  19871  metustrelOLD  20135  metustrel  20136  xppreima2  25970  df1stres  26004  df2ndres  26005  f1od2  26029  fpwrelmap  26038  metideq  26325  metider  26326  pstmfval  26328  xpinpreima2  26342  tpr2rico  26347  dya2iocnrect  26701  txprel  27915  mblfinlem1  28433  bj-elid  32526  dihvalrel  34929
  Copyright terms: Public domain W3C validator