Theorem xpss12 4771

Description: Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
xpss12	|- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Proof of Theorem xpss12

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3178	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3178	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 598	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 4314	. 2 |- ( ( A C_ B /\ C C_ D ) -> { <. x , y >. | ( x e. A /\ y e. C ) } C_ { <. x , y >. | ( x e. B /\ y e. D ) } )
5		df-xp 4670	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4670	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3227	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2167   C_ wss 3157   {copab 4094   X. cxp 4662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-in 3163  df-ss 3170  df-opab 4096  df-xp 4670

This theorem is referenced by:  xpss  4772  xpss1  4774  xpss2  4775  djussxp  4812  ssxpbm  5106  ssrnres  5113  cossxp  5193  cossxp2  5194  cocnvss  5196  relrelss  5197  fssxp  5428  oprabss  6012  pmss12g  6743  caserel  7162  casef  7163  dmaddpi  7411  dmmulpi  7412  rexpssxrxp  8090  ltrelxr  8106  dfz2  9417  phimullem  12420  znleval  14287  txuni2  14600  txbas  14602  neitx  14612  txcnp  14615  cnmpt2res  14641  psmetres2  14677  xmetres2  14723  metres2  14725  xmetresbl  14784  xmettx  14854  qtopbasss  14865  tgqioo  14899  resubmet  14900  limccnp2lem  15020  limccnp2cntop  15021  mpodvdsmulf1o  15334  fsumdvdsmul  15335