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

Theorem xpss2 5219
Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.)
Assertion
Ref Expression
xpss2 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))

Proof of Theorem xpss2
StepHypRef Expression
1 ssid 3616 . 2 𝐶𝐶
2 xpss12 5215 . 2 ((𝐶𝐶𝐴𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
31, 2mpan 705 1 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3567   × cxp 5102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-in 3574  df-ss 3581  df-opab 4704  df-xp 5110
This theorem is referenced by:  xpdom3  8043  marypha1lem  8324  unctb  9012  axresscn  9954  imasvscafn  16178  imasvscaf  16180  xpsc0  16201  xpsc1  16202  gass  17715  gsum2d  18352  tx2cn  21394  txtube  21424  txcmplem1  21425  hausdiag  21429  xkoinjcn  21471  caussi  23076  dvfval  23642  issh2  28036  qtophaus  29877  2ndmbfm  30297  sxbrsigalem0  30307  cvmlift2lem9  31267  cvmlift2lem11  31269  filnetlem3  32350  trclexi  37746  cnvtrcl0  37752  ovolval5lem2  40630  ovnovollem1  40633  ovnovollem2  40634
  Copyright terms: Public domain W3C validator