Theorem xpss12 5647

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	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))

Proof of Theorem xpss12

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3929	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssel 3929	. . . 4 ⊢ (𝐶 ⊆ 𝐷 → (𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))
3	1, 2	im2anan9 621	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
4	3	ssopab2dv 5507	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)})
5		df-xp 5638	. 2 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
6		df-xp 5638	. 2 ⊢ (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)}
7	4, 5, 6	3sstr4g 3989	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3903  {copab 5162   × cxp 5630

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-opab 5163  df-xp 5638

This theorem is referenced by:  xpss  5648  inxpssres  5649  xpss1  5651  xpss2  5652  djussxp  5802  ssxpb  6140  resssxp  6236  cossxp  6238  relrelss  6239  fssxp  6697  oprabss  7476  oprres  7536  fimaproj  8087  xpord2pred  8097  xpord3pred  8104  naddcllem  8614  naddov2  8617  naddunif  8631  naddasslem1  8632  naddasslem2  8633  pmss12g  8819  marypha1lem  9348  marypha2lem1  9350  hartogslem1  9459  infxpenlem  9935  dfac5lem4  10048  dfac5lem4OLD  10050  axdc4lem  10377  fpwwe2lem1  10554  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2lem12  10565  canthwe  10574  tskxpss  10695  dmaddpi  10813  dmmulpi  10814  addnqf  10871  mulnqf  10872  rexpssxrxp  11189  ltrelxr  11205  mulnzcnf  11795  dfz2  12519  elq  12875  leiso  14394  znnen  16149  phimullem  16718  imasless  17473  sscpwex  17751  fullsubc  17786  fullresc  17787  wunfunc  17837  funcres2c  17839  homaf  17966  dmcoass  18002  catcoppccl  18053  catcfuccl  18054  catcxpccl  18142  rnghmresfn  20564  rnghmsscmap2  20574  rnghmsscmap  20575  rhmresfn  20593  rhmsscmap2  20603  rhmsscmap  20604  rhmsscrnghm  20610  rngcrescrhm  20629  znleval  21521  txuni2  23521  txbas  23523  txcld  23559  txcls  23560  neitx  23563  txcnp  23576  txlly  23592  txnlly  23593  hausdiag  23601  tx1stc  23606  txkgen  23608  xkococnlem  23615  cnmpt2res  23633  clssubg  24065  tsmsxplem1  24109  tsmsxplem2  24110  tsmsxp  24111  trust  24185  ustuqtop1  24197  psmetres2  24270  xmetres2  24317  metres2  24319  ressprdsds  24327  xmetresbl  24393  ressxms  24481  metustexhalf  24512  cfilucfil  24515  restmetu  24526  nrginvrcn  24648  qtopbaslem  24714  tgqioo  24756  re2ndc  24757  resubmet  24758  xrsdsre  24767  bndth  24925  lebnumii  24933  iscfil2  25234  cmssmscld  25318  cmsss  25319  cmscsscms  25341  minveclem3a  25395  ovolfsf  25440  opnmblALT  25572  mbfimaopnlem  25624  itg1addlem4  25668  limccnp2  25861  taylfval  26334  taylf  26336  mpodvdsmulf1o  27172  fsumdvdsmul  27173  dvdsmulf1o  27174  fsumdvdsmulOLD  27175  elzs  28392  sspg  30815  ssps  30817  sspmlem  30819  issh2  31296  hhssabloilem  31348  hhssabloi  31349  hhssnv  31351  hhshsslem1  31354  shsel  31401  iunxpssiun1  32654  ofrn2  32729  djussxp2  32737  gtiso  32790  xrofsup  32857  gsumwrd2dccatlem  33170  txomap  34011  tpr2rico  34089  prsss  34093  raddcn  34106  xrge0pluscn  34117  br2base  34446  dya2iocnrect  34458  dya2iocucvr  34461  eulerpartlemgh  34555  eulerpartlemgs2  34557  cvmlift2lem9  35524  cvmlift2lem10  35525  cvmlift2lem11  35526  cvmlift2lem12  35527  mpstssv  35752  elxp8  37620  mblfinlem2  37903  ftc1anc  37946  ssbnd  38033  prdsbnd2  38040  cnpwstotbnd  38042  reheibor  38084  exidreslem  38122  divrngcl  38202  isdrngo2  38203  dibss  41539  xppss12  42595  arearect  43566  rtrclex  43967  rtrclexi  43971  rr2sscn2  45718  fourierdlem42  46501  opnvonmbllem2  46985  rngcrescrhmALTV  48634  imaidfu  49463  imasubc  49504