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

Theorem xpss 5539
 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 (𝐴 × 𝐵) ⊆ (V × V)

Proof of Theorem xpss
StepHypRef Expression
1 ssv 3942 . 2 𝐴 ⊆ V
2 ssv 3942 . 2 𝐵 ⊆ V
3 xpss12 5538 . 2 ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V))
41, 2, 3mp2an 691 1 (𝐴 × 𝐵) ⊆ (V × V)
 Colors of variables: wff setvar class Syntax hints:  Vcvv 3444   ⊆ wss 3884   × cxp 5521 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-opab 5096  df-xp 5529 This theorem is referenced by:  relxp  5541  copsex2ga  5648  eqbrrdva  5708  relrelss  6096  dff3  6847  eqopi  7711  op1steq  7719  dfoprab4  7739  infxpenlem  9428  nqerf  10345  uzrdgfni  13325  reltrclfv  14372  homarel  17292  relxpchom  17427  frmdplusg  18015  upxp  22232  ustrel  22821  utop2nei  22860  utop3cls  22861  fmucndlem  22901  metustrel  23163  xppreima2  30417  df1stres  30467  df2ndres  30468  f1od2  30487  fsuppcurry1  30491  fsuppcurry2  30492  fpwrelmap  30499  metideq  31250  metider  31251  pstmfval  31253  xpinpreima2  31264  tpr2rico  31269  esum2d  31466  dya2iocnrect  31653  mpstssv  32900  txprel  33454  elxp8  34789  mblfinlem1  35093  xrnrel  35784  dihvalrel  38574  rfovcnvf1od  40698  ovolval2lem  43275  sprsymrelfo  44007
 Copyright terms: Public domain W3C validator