Theorem xpss12 5638

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3905  {copab 5157   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3922  df-opab 5158  df-xp 5629

This theorem is referenced by:  xpss  5639  inxpssres  5640  xpss1  5642  xpss2  5643  djussxp  5792  ssxpb  6127  resssxp  6222  cossxp  6224  relrelss  6225  fssxp  6683  oprabss  7461  oprres  7521  fimaproj  8075  xpord2pred  8085  xpord3pred  8092  naddcllem  8601  naddov2  8604  naddunif  8618  naddasslem1  8619  naddasslem2  8620  pmss12g  8803  marypha1lem  9342  marypha2lem1  9344  hartogslem1  9453  infxpenlem  9926  dfac5lem4  10039  dfac5lem4OLD  10041  axdc4lem  10368  fpwwe2lem1  10544  fpwwe2lem10  10553  fpwwe2lem11  10554  fpwwe2lem12  10555  canthwe  10564  tskxpss  10685  dmaddpi  10803  dmmulpi  10804  addnqf  10861  mulnqf  10862  rexpssxrxp  11179  ltrelxr  11195  mulnzcnf  11784  dfz2  12508  elq  12869  leiso  14384  znnen  16139  phimullem  16708  imasless  17462  sscpwex  17740  fullsubc  17775  fullresc  17776  wunfunc  17826  funcres2c  17828  homaf  17955  dmcoass  17991  catcoppccl  18042  catcfuccl  18043  catcxpccl  18131  rnghmresfn  20522  rnghmsscmap2  20532  rnghmsscmap  20533  rhmresfn  20551  rhmsscmap2  20561  rhmsscmap  20562  rhmsscrnghm  20568  rngcrescrhm  20587  znleval  21479  txuni2  23468  txbas  23470  txcld  23506  txcls  23507  neitx  23510  txcnp  23523  txlly  23539  txnlly  23540  hausdiag  23548  tx1stc  23553  txkgen  23555  xkococnlem  23562  cnmpt2res  23580  clssubg  24012  tsmsxplem1  24056  tsmsxplem2  24057  tsmsxp  24058  trust  24133  ustuqtop1  24145  psmetres2  24218  xmetres2  24265  metres2  24267  ressprdsds  24275  xmetresbl  24341  ressxms  24429  metustexhalf  24460  cfilucfil  24463  restmetu  24474  nrginvrcn  24596  qtopbaslem  24662  tgqioo  24704  re2ndc  24705  resubmet  24706  xrsdsre  24715  bndth  24873  lebnumii  24881  iscfil2  25182  cmssmscld  25266  cmsss  25267  cmscsscms  25289  minveclem3a  25343  ovolfsf  25388  opnmblALT  25520  mbfimaopnlem  25572  itg1addlem4  25616  limccnp2  25809  taylfval  26282  taylf  26284  mpodvdsmulf1o  27120  fsumdvdsmul  27121  dvdsmulf1o  27122  fsumdvdsmulOLD  27123  elzs  28295  sspg  30690  ssps  30692  sspmlem  30694  issh2  31171  hhssabloilem  31223  hhssabloi  31224  hhssnv  31226  hhshsslem1  31229  shsel  31276  iunxpssiun1  32530  ofrn2  32597  djussxp2  32605  gtiso  32657  xrofsup  32723  gsumwrd2dccatlem  33032  txomap  33800  tpr2rico  33878  prsss  33882  raddcn  33895  xrge0pluscn  33906  br2base  34236  dya2iocnrect  34248  dya2iocucvr  34251  eulerpartlemgh  34345  eulerpartlemgs2  34347  cvmlift2lem9  35283  cvmlift2lem10  35284  cvmlift2lem11  35285  cvmlift2lem12  35286  mpstssv  35511  elxp8  37344  mblfinlem2  37637  ftc1anc  37680  ssbnd  37767  prdsbnd2  37774  cnpwstotbnd  37776  reheibor  37818  exidreslem  37856  divrngcl  37936  isdrngo2  37937  dibss  41148  xppss12  42202  arearect  43188  rtrclex  43590  rtrclexi  43594  rr2sscn2  45346  fourierdlem42  46131  opnvonmbllem2  46615  rngcrescrhmALTV  48265  imaidfu  49096  imasubc  49137