Theorem xpss12 5634

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3898  {copab 5155   × cxp 5617

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-opab 5156  df-xp 5625

This theorem is referenced by:  xpss  5635  inxpssres  5636  xpss1  5638  xpss2  5639  djussxp  5789  ssxpb  6126  resssxp  6222  cossxp  6224  relrelss  6225  fssxp  6683  oprabss  7460  oprres  7520  fimaproj  8071  xpord2pred  8081  xpord3pred  8088  naddcllem  8597  naddov2  8600  naddunif  8614  naddasslem1  8615  naddasslem2  8616  pmss12g  8799  marypha1lem  9324  marypha2lem1  9326  hartogslem1  9435  infxpenlem  9911  dfac5lem4  10024  dfac5lem4OLD  10026  axdc4lem  10353  fpwwe2lem1  10529  fpwwe2lem10  10538  fpwwe2lem11  10539  fpwwe2lem12  10540  canthwe  10549  tskxpss  10670  dmaddpi  10788  dmmulpi  10789  addnqf  10846  mulnqf  10847  rexpssxrxp  11164  ltrelxr  11180  mulnzcnf  11770  dfz2  12494  elq  12850  leiso  14368  znnen  16123  phimullem  16692  imasless  17446  sscpwex  17724  fullsubc  17759  fullresc  17760  wunfunc  17810  funcres2c  17812  homaf  17939  dmcoass  17975  catcoppccl  18026  catcfuccl  18027  catcxpccl  18115  rnghmresfn  20536  rnghmsscmap2  20546  rnghmsscmap  20547  rhmresfn  20565  rhmsscmap2  20575  rhmsscmap  20576  rhmsscrnghm  20582  rngcrescrhm  20601  znleval  21493  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  30710  ssps  30712  sspmlem  30714  issh2  31191  hhssabloilem  31243  hhssabloi  31244  hhssnv  31246  hhshsslem1  31249  shsel  31296  iunxpssiun1  32550  ofrn2  32624  djussxp2  32632  gtiso  32686  xrofsup  32754  gsumwrd2dccatlem  33053  txomap  33868  tpr2rico  33946  prsss  33950  raddcn  33963  xrge0pluscn  33974  br2base  34303  dya2iocnrect  34315  dya2iocucvr  34318  eulerpartlemgh  34412  eulerpartlemgs2  34414  cvmlift2lem9  35376  cvmlift2lem10  35377  cvmlift2lem11  35378  cvmlift2lem12  35379  mpstssv  35604  elxp8  37436  mblfinlem2  37719  ftc1anc  37762  ssbnd  37849  prdsbnd2  37856  cnpwstotbnd  37858  reheibor  37900  exidreslem  37938  divrngcl  38018  isdrngo2  38019  dibss  41289  xppss12  42348  arearect  43333  rtrclex  43735  rtrclexi  43739  rr2sscn2  45489  fourierdlem42  46272  opnvonmbllem2  46756  rngcrescrhmALTV  48405  imaidfu  49236  imasubc  49277