Theorem xpss12 5631

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 3928	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssel 3928	. . . 4 ⊢ (𝐶 ⊆ 𝐷 → (𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷))
3	1, 2	im2anan9 620	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
4	3	ssopab2dv 5491	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)})
5		df-xp 5622	. 2 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
6		df-xp 5622	. 2 ⊢ (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)}
7	4, 5, 6	3sstr4g 3988	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ⊆ wss 3902  {copab 5153   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3919  df-opab 5154  df-xp 5622

This theorem is referenced by:  xpss  5632  inxpssres  5633  xpss1  5635  xpss2  5636  djussxp  5785  ssxpb  6121  resssxp  6217  cossxp  6219  relrelss  6220  fssxp  6678  oprabss  7454  oprres  7514  fimaproj  8065  xpord2pred  8075  xpord3pred  8082  naddcllem  8591  naddov2  8594  naddunif  8608  naddasslem1  8609  naddasslem2  8610  pmss12g  8793  marypha1lem  9317  marypha2lem1  9319  hartogslem1  9428  infxpenlem  9904  dfac5lem4  10017  dfac5lem4OLD  10019  axdc4lem  10346  fpwwe2lem1  10522  fpwwe2lem10  10531  fpwwe2lem11  10532  fpwwe2lem12  10533  canthwe  10542  tskxpss  10663  dmaddpi  10781  dmmulpi  10782  addnqf  10839  mulnqf  10840  rexpssxrxp  11157  ltrelxr  11173  mulnzcnf  11763  dfz2  12487  elq  12848  leiso  14366  znnen  16121  phimullem  16690  imasless  17444  sscpwex  17722  fullsubc  17757  fullresc  17758  wunfunc  17808  funcres2c  17810  homaf  17937  dmcoass  17973  catcoppccl  18024  catcfuccl  18025  catcxpccl  18113  rnghmresfn  20535  rnghmsscmap2  20545  rnghmsscmap  20546  rhmresfn  20564  rhmsscmap2  20574  rhmsscmap  20575  rhmsscrnghm  20581  rngcrescrhm  20600  znleval  21492  txuni2  23481  txbas  23483  txcld  23519  txcls  23520  neitx  23523  txcnp  23536  txlly  23552  txnlly  23553  hausdiag  23561  tx1stc  23566  txkgen  23568  xkococnlem  23575  cnmpt2res  23593  clssubg  24025  tsmsxplem1  24069  tsmsxplem2  24070  tsmsxp  24071  trust  24145  ustuqtop1  24157  psmetres2  24230  xmetres2  24277  metres2  24279  ressprdsds  24287  xmetresbl  24353  ressxms  24441  metustexhalf  24472  cfilucfil  24475  restmetu  24486  nrginvrcn  24608  qtopbaslem  24674  tgqioo  24716  re2ndc  24717  resubmet  24718  xrsdsre  24727  bndth  24885  lebnumii  24893  iscfil2  25194  cmssmscld  25278  cmsss  25279  cmscsscms  25301  minveclem3a  25355  ovolfsf  25400  opnmblALT  25532  mbfimaopnlem  25584  itg1addlem4  25628  limccnp2  25821  taylfval  26294  taylf  26296  mpodvdsmulf1o  27132  fsumdvdsmul  27133  dvdsmulf1o  27134  fsumdvdsmulOLD  27135  elzs  28309  sspg  30706  ssps  30708  sspmlem  30710  issh2  31187  hhssabloilem  31239  hhssabloi  31240  hhssnv  31242  hhshsslem1  31245  shsel  31292  iunxpssiun1  32546  ofrn2  32620  djussxp2  32628  gtiso  32680  xrofsup  32748  gsumwrd2dccatlem  33044  txomap  33845  tpr2rico  33923  prsss  33927  raddcn  33940  xrge0pluscn  33951  br2base  34280  dya2iocnrect  34292  dya2iocucvr  34295  eulerpartlemgh  34389  eulerpartlemgs2  34391  cvmlift2lem9  35353  cvmlift2lem10  35354  cvmlift2lem11  35355  cvmlift2lem12  35356  mpstssv  35581  elxp8  37411  mblfinlem2  37704  ftc1anc  37747  ssbnd  37834  prdsbnd2  37841  cnpwstotbnd  37843  reheibor  37885  exidreslem  37923  divrngcl  38003  isdrngo2  38004  dibss  41214  xppss12  42268  arearect  43254  rtrclex  43656  rtrclexi  43660  rr2sscn2  45410  fourierdlem42  46193  opnvonmbllem2  46677  rngcrescrhmALTV  48317  imaidfu  49148  imasubc  49189