Theorem xpss12 5595

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3883  {copab 5132   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586

This theorem is referenced by:  xpss  5596  inxpssres  5597  xpss1  5599  xpss2  5600  djussxp  5743  ssxpb  6066  resssxp  6162  cossxp  6164  relrelss  6165  fssxp  6612  oprabss  7359  oprres  7418  fimaproj  7947  pmss12g  8615  marypha1lem  9122  marypha2lem1  9124  hartogslem1  9231  infxpenlem  9700  dfac5lem4  9813  axdc4lem  10142  fpwwe2lem1  10318  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe2lem12  10329  canthwe  10338  tskxpss  10459  dmaddpi  10577  dmmulpi  10578  addnqf  10635  mulnqf  10636  rexpssxrxp  10951  ltrelxr  10967  mulnzcnopr  11551  dfz2  12268  elq  12619  leiso  14101  znnen  15849  phimullem  16408  imasless  17168  sscpwex  17444  fullsubc  17481  fullresc  17482  wunfunc  17530  wunfuncOLD  17531  funcres2c  17533  homaf  17661  dmcoass  17697  catcoppccl  17748  catcoppcclOLD  17749  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  znleval  20674  txuni2  22624  txbas  22626  txcld  22662  txcls  22663  neitx  22666  txcnp  22679  txlly  22695  txnlly  22696  hausdiag  22704  tx1stc  22709  txkgen  22711  xkococnlem  22718  cnmpt2res  22736  clssubg  23168  tsmsxplem1  23212  tsmsxplem2  23213  tsmsxp  23214  trust  23289  ustuqtop1  23301  psmetres2  23375  xmetres2  23422  metres2  23424  ressprdsds  23432  xmetresbl  23498  ressxms  23587  metustexhalf  23618  cfilucfil  23621  restmetu  23632  nrginvrcn  23762  qtopbaslem  23828  tgqioo  23869  re2ndc  23870  resubmet  23871  xrsdsre  23879  bndth  24027  lebnumii  24035  iscfil2  24335  cmssmscld  24419  cmsss  24420  cmscsscms  24442  minveclem3a  24496  ovolfsf  24540  opnmblALT  24672  mbfimaopnlem  24724  itg1addlem4  24768  itg1addlem4OLD  24769  limccnp2  24961  taylfval  25423  taylf  25425  dvdsmulf1o  26248  fsumdvdsmul  26249  sspg  28991  ssps  28993  sspmlem  28995  issh2  29472  hhssabloilem  29524  hhssabloi  29525  hhssnv  29527  hhshsslem1  29530  shsel  29577  ofrn2  30878  djussxp2  30886  gtiso  30935  xrofsup  30992  txomap  31686  tpr2rico  31764  prsss  31768  raddcn  31781  xrge0pluscn  31792  br2base  32136  dya2iocnrect  32148  dya2iocucvr  32151  eulerpartlemgh  32245  eulerpartlemgs2  32247  cvmlift2lem9  33173  cvmlift2lem10  33174  cvmlift2lem11  33175  cvmlift2lem12  33176  mpstssv  33401  xpord2pred  33719  xpord3pred  33725  naddcllem  33758  naddov2  33761  addscllem1  34058  elxp8  35469  mblfinlem2  35742  ftc1anc  35785  ssbnd  35873  prdsbnd2  35880  cnpwstotbnd  35882  reheibor  35924  exidreslem  35962  divrngcl  36042  isdrngo2  36043  dibss  39110  xppss12  40130  arearect  40962  rtrclex  41114  rtrclexi  41118  rr2sscn2  42795  fourierdlem42  43580  opnvonmbllem2  44061  rnghmresfn  45409  rnghmsscmap2  45419  rnghmsscmap  45420  rhmresfn  45455  rhmsscmap2  45465  rhmsscmap  45466  rhmsscrnghm  45472  rngcrescrhm  45531  rngcrescrhmALTV  45549