Theorem xpss12 5225

Description: Subset theorem for Cartesian 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 3597	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3597	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 880	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 5004	. 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 5120	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 5120	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3646	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   C_ wss 3574   {copab 4712   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-opab 4713  df-xp 5120

This theorem is referenced by:  xpss  5226  xpss1  5228  xpss2  5229  djussxp  5267  ssxpb  5568  ssrnres  5572  cossxp  5658  relrelss  5659  fssxp  6060  oprabss  6746  oprres  6802  pmss12g  7884  marypha1lem  8339  marypha2lem1  8341  hartogslem1  8447  infxpenlem  8836  dfac5lem4  8949  axdc4lem  9277  fpwwe2lem1  9453  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2lem13  9464  canthwe  9473  tskxpss  9594  dmaddpi  9712  dmmulpi  9713  addnqf  9770  mulnqf  9771  rexpssxrxp  10084  ltrelxr  10099  mulnzcnopr  10673  dfz2  11395  elq  11790  leiso  13243  znnen  14941  eucalg  15300  phimullem  15484  imasless  16200  sscpwex  16475  fullsubc  16510  fullresc  16511  wunfunc  16559  funcres2c  16561  homaf  16680  dmcoass  16716  catcoppccl  16758  catcfuccl  16759  catcxpccl  16847  znleval  19903  txuni2  21368  txbas  21370  txcld  21406  txcls  21407  neitx  21410  txcnp  21423  txlly  21439  txnlly  21440  hausdiag  21448  tx1stc  21453  txkgen  21455  xkococnlem  21462  cnmpt2res  21480  clssubg  21912  tsmsxplem1  21956  tsmsxplem2  21957  tsmsxp  21958  trust  22033  ustuqtop1  22045  psmetres2  22119  xmetres2  22166  metres2  22168  ressprdsds  22176  xmetresbl  22242  ressxms  22330  metustexhalf  22361  cfilucfil  22364  restmetu  22375  nrginvrcn  22496  qtopbaslem  22562  tgqioo  22603  re2ndc  22604  resubmet  22605  xrsdsre  22613  bndth  22757  lebnumii  22765  iscfil2  23064  cmsss  23147  minveclem3a  23198  ovolfsf  23240  opnmblALT  23371  mbfimaopnlem  23422  itg1addlem4  23466  limccnp2  23656  taylfval  24113  taylf  24115  dvdsmulf1o  24920  fsumdvdsmul  24921  sspg  27583  ssps  27585  sspmlem  27587  issh2  28066  hhssabloilem  28118  hhssabloi  28119  hhssnv  28121  hhshsslem1  28124  shsel  28173  ofrn2  29442  gtiso  29478  xrofsup  29533  fimaproj  29900  txomap  29901  tpr2rico  29958  prsss  29962  raddcn  29975  xrge0pluscn  29986  br2base  30331  dya2iocnrect  30343  dya2iocucvr  30346  eulerpartlemgh  30440  eulerpartlemgs2  30442  cvmlift2lem9  31293  cvmlift2lem10  31294  cvmlift2lem11  31295  cvmlift2lem12  31296  mpstssv  31436  elxp8  33219  mblfinlem2  33447  ftc1anc  33493  ssbnd  33587  prdsbnd2  33594  cnpwstotbnd  33596  reheibor  33638  exidreslem  33676  divrngcl  33756  isdrngo2  33757  inxpssres  34076  dibss  36458  arearect  37801  rtrclex  37924  rtrclexi  37928  rp-imass  38065  idhe  38081  rr2sscn2  39582  fourierdlem42  40366  opnvonmbllem2  40847  rnghmresfn  41963  rnghmsscmap2  41973  rnghmsscmap  41974  rhmresfn  42009  rhmsscmap2  42019  rhmsscmap  42020  rhmsscrnghm  42026  rngcrescrhm  42085  rngcrescrhmALTV  42103