Theorem xpss12 5646

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3889  {copab 5147   × cxp 5629

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-opab 5148  df-xp 5637

This theorem is referenced by:  xpss  5647  inxpssres  5648  xpss1  5650  xpss2  5651  djussxp  5800  ssxpb  6138  resssxp  6234  cossxp  6236  relrelss  6237  fssxp  6695  oprabss  7475  oprres  7535  fimaproj  8085  xpord2pred  8095  xpord3pred  8102  naddcllem  8612  naddov2  8615  naddunif  8629  naddasslem1  8630  naddasslem2  8631  pmss12g  8817  marypha1lem  9346  marypha2lem1  9348  hartogslem1  9457  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  11190  ltrelxr  11206  mulnzcnf  11796  dfz2  12543  elq  12900  leiso  14421  znnen  16179  phimullem  16749  imasless  17504  sscpwex  17782  fullsubc  17817  fullresc  17818  wunfunc  17868  funcres2c  17870  homaf  17997  dmcoass  18033  catcoppccl  18084  catcfuccl  18085  catcxpccl  18173  rnghmresfn  20596  rnghmsscmap2  20606  rnghmsscmap  20607  rhmresfn  20625  rhmsscmap2  20635  rhmsscmap  20636  rhmsscrnghm  20642  rngcrescrhm  20661  znleval  21534  txuni2  23530  txbas  23532  txcld  23568  txcls  23569  neitx  23572  txcnp  23585  txlly  23601  txnlly  23602  hausdiag  23610  tx1stc  23615  txkgen  23617  xkococnlem  23624  cnmpt2res  23642  clssubg  24074  tsmsxplem1  24118  tsmsxplem2  24119  tsmsxp  24120  trust  24194  ustuqtop1  24206  psmetres2  24279  xmetres2  24326  metres2  24328  ressprdsds  24336  xmetresbl  24402  ressxms  24490  metustexhalf  24521  cfilucfil  24524  restmetu  24535  nrginvrcn  24657  qtopbaslem  24723  tgqioo  24765  re2ndc  24766  resubmet  24767  xrsdsre  24776  bndth  24925  lebnumii  24933  iscfil2  25233  cmssmscld  25317  cmsss  25318  cmscsscms  25340  minveclem3a  25394  ovolfsf  25438  opnmblALT  25570  mbfimaopnlem  25622  itg1addlem4  25666  limccnp2  25859  taylfval  26324  taylf  26326  mpodvdsmulf1o  27157  fsumdvdsmul  27158  dvdsmulf1o  27159  elzs  28376  sspg  30799  ssps  30801  sspmlem  30803  issh2  31280  hhssabloilem  31332  hhssabloi  31333  hhssnv  31335  hhshsslem1  31338  shsel  31385  iunxpssiun1  32638  ofrn2  32713  djussxp2  32721  gtiso  32774  xrofsup  32840  gsumwrd2dccatlem  33138  txomap  33978  tpr2rico  34056  prsss  34060  raddcn  34073  xrge0pluscn  34084  br2base  34413  dya2iocnrect  34425  dya2iocucvr  34428  eulerpartlemgh  34522  eulerpartlemgs2  34524  cvmlift2lem9  35493  cvmlift2lem10  35494  cvmlift2lem11  35495  cvmlift2lem12  35496  mpstssv  35721  elxp8  37687  mblfinlem2  37979  ftc1anc  38022  ssbnd  38109  prdsbnd2  38116  cnpwstotbnd  38118  reheibor  38160  exidreslem  38198  divrngcl  38278  isdrngo2  38279  dibss  41615  xppss12  42670  arearect  43643  rtrclex  44044  rtrclexi  44048  rr2sscn2  45795  fourierdlem42  46577  opnvonmbllem2  47061  rngcrescrhmALTV  48756  imaidfu  49585  imasubc  49626