Theorem xpss12 5639

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3901  {copab 5160   × cxp 5622

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpss  5640  inxpssres  5641  xpss1  5643  xpss2  5644  djussxp  5794  ssxpb  6132  resssxp  6228  cossxp  6230  relrelss  6231  fssxp  6689  oprabss  7466  oprres  7526  fimaproj  8077  xpord2pred  8087  xpord3pred  8094  naddcllem  8604  naddov2  8607  naddunif  8621  naddasslem1  8622  naddasslem2  8623  pmss12g  8807  marypha1lem  9336  marypha2lem1  9338  hartogslem1  9447  infxpenlem  9923  dfac5lem4  10036  dfac5lem4OLD  10038  axdc4lem  10365  fpwwe2lem1  10542  fpwwe2lem10  10551  fpwwe2lem11  10552  fpwwe2lem12  10553  canthwe  10562  tskxpss  10683  dmaddpi  10801  dmmulpi  10802  addnqf  10859  mulnqf  10860  rexpssxrxp  11177  ltrelxr  11193  mulnzcnf  11783  dfz2  12507  elq  12863  leiso  14382  znnen  16137  phimullem  16706  imasless  17461  sscpwex  17739  fullsubc  17774  fullresc  17775  wunfunc  17825  funcres2c  17827  homaf  17954  dmcoass  17990  catcoppccl  18041  catcfuccl  18042  catcxpccl  18130  rnghmresfn  20552  rnghmsscmap2  20562  rnghmsscmap  20563  rhmresfn  20581  rhmsscmap2  20591  rhmsscmap  20592  rhmsscrnghm  20598  rngcrescrhm  20617  znleval  21509  txuni2  23509  txbas  23511  txcld  23547  txcls  23548  neitx  23551  txcnp  23564  txlly  23580  txnlly  23581  hausdiag  23589  tx1stc  23594  txkgen  23596  xkococnlem  23603  cnmpt2res  23621  clssubg  24053  tsmsxplem1  24097  tsmsxplem2  24098  tsmsxp  24099  trust  24173  ustuqtop1  24185  psmetres2  24258  xmetres2  24305  metres2  24307  ressprdsds  24315  xmetresbl  24381  ressxms  24469  metustexhalf  24500  cfilucfil  24503  restmetu  24514  nrginvrcn  24636  qtopbaslem  24702  tgqioo  24744  re2ndc  24745  resubmet  24746  xrsdsre  24755  bndth  24913  lebnumii  24921  iscfil2  25222  cmssmscld  25306  cmsss  25307  cmscsscms  25329  minveclem3a  25383  ovolfsf  25428  opnmblALT  25560  mbfimaopnlem  25612  itg1addlem4  25656  limccnp2  25849  taylfval  26322  taylf  26324  mpodvdsmulf1o  27160  fsumdvdsmul  27161  dvdsmulf1o  27162  fsumdvdsmulOLD  27163  elzs  28380  sspg  30803  ssps  30805  sspmlem  30807  issh2  31284  hhssabloilem  31336  hhssabloi  31337  hhssnv  31339  hhshsslem1  31342  shsel  31389  iunxpssiun1  32643  ofrn2  32718  djussxp2  32726  gtiso  32780  xrofsup  32847  gsumwrd2dccatlem  33159  txomap  33991  tpr2rico  34069  prsss  34073  raddcn  34086  xrge0pluscn  34097  br2base  34426  dya2iocnrect  34438  dya2iocucvr  34441  eulerpartlemgh  34535  eulerpartlemgs2  34537  cvmlift2lem9  35505  cvmlift2lem10  35506  cvmlift2lem11  35507  cvmlift2lem12  35508  mpstssv  35733  elxp8  37572  mblfinlem2  37855  ftc1anc  37898  ssbnd  37985  prdsbnd2  37992  cnpwstotbnd  37994  reheibor  38036  exidreslem  38074  divrngcl  38154  isdrngo2  38155  dibss  41425  xppss12  42481  arearect  43453  rtrclex  43854  rtrclexi  43858  rr2sscn2  45606  fourierdlem42  46389  opnvonmbllem2  46873  rngcrescrhmALTV  48522  imaidfu  49351  imasubc  49392