Theorem xpss12 5680

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107   ⊆ wss 3931  {copab 5185   × cxp 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ss 3948  df-opab 5186  df-xp 5671

This theorem is referenced by:  xpss  5681  inxpssres  5682  xpss1  5684  xpss2  5685  djussxp  5836  ssxpb  6174  resssxp  6270  cossxp  6272  relrelss  6273  fssxp  6743  oprabss  7523  oprres  7583  fimaproj  8142  xpord2pred  8152  xpord3pred  8159  naddcllem  8696  naddov2  8699  naddunif  8713  naddasslem1  8714  naddasslem2  8715  pmss12g  8891  marypha1lem  9455  marypha2lem1  9457  hartogslem1  9564  infxpenlem  10035  dfac5lem4  10148  dfac5lem4OLD  10150  axdc4lem  10477  fpwwe2lem1  10653  fpwwe2lem10  10662  fpwwe2lem11  10663  fpwwe2lem12  10664  canthwe  10673  tskxpss  10794  dmaddpi  10912  dmmulpi  10913  addnqf  10970  mulnqf  10971  rexpssxrxp  11288  ltrelxr  11304  mulnzcnf  11891  dfz2  12615  elq  12974  leiso  14481  znnen  16231  phimullem  16799  imasless  17557  sscpwex  17831  fullsubc  17867  fullresc  17868  wunfunc  17918  funcres2c  17920  homaf  18047  dmcoass  18083  catcoppccl  18134  catcfuccl  18135  catcxpccl  18223  rnghmresfn  20588  rnghmsscmap2  20598  rnghmsscmap  20599  rhmresfn  20617  rhmsscmap2  20627  rhmsscmap  20628  rhmsscrnghm  20634  rngcrescrhm  20653  znleval  21528  txuni2  23520  txbas  23522  txcld  23558  txcls  23559  neitx  23562  txcnp  23575  txlly  23591  txnlly  23592  hausdiag  23600  tx1stc  23605  txkgen  23607  xkococnlem  23614  cnmpt2res  23632  clssubg  24064  tsmsxplem1  24108  tsmsxplem2  24109  tsmsxp  24110  trust  24185  ustuqtop1  24197  psmetres2  24270  xmetres2  24317  metres2  24319  ressprdsds  24327  xmetresbl  24393  ressxms  24483  metustexhalf  24514  cfilucfil  24517  restmetu  24528  nrginvrcn  24650  qtopbaslem  24716  tgqioo  24758  re2ndc  24759  resubmet  24760  xrsdsre  24769  bndth  24927  lebnumii  24935  iscfil2  25237  cmssmscld  25321  cmsss  25322  cmscsscms  25344  minveclem3a  25398  ovolfsf  25443  opnmblALT  25575  mbfimaopnlem  25627  itg1addlem4  25671  limccnp2  25864  taylfval  26337  taylf  26339  mpodvdsmulf1o  27174  fsumdvdsmul  27175  dvdsmulf1o  27176  fsumdvdsmulOLD  27177  elzs  28307  sspg  30676  ssps  30678  sspmlem  30680  issh2  31157  hhssabloilem  31209  hhssabloi  31210  hhssnv  31212  hhshsslem1  31215  shsel  31262  iunxpssiun1  32517  ofrn2  32586  djussxp2  32594  gtiso  32646  xrofsup  32713  gsumwrd2dccatlem  33013  txomap  33808  tpr2rico  33886  prsss  33890  raddcn  33903  xrge0pluscn  33914  br2base  34246  dya2iocnrect  34258  dya2iocucvr  34261  eulerpartlemgh  34355  eulerpartlemgs2  34357  cvmlift2lem9  35291  cvmlift2lem10  35292  cvmlift2lem11  35293  cvmlift2lem12  35294  mpstssv  35519  elxp8  37347  mblfinlem2  37640  ftc1anc  37683  ssbnd  37770  prdsbnd2  37777  cnpwstotbnd  37779  reheibor  37821  exidreslem  37859  divrngcl  37939  isdrngo2  37940  dibss  41146  xppss12  42243  arearect  43205  rtrclex  43607  rtrclexi  43611  rr2sscn2  45349  fourierdlem42  46136  opnvonmbllem2  46620  rngcrescrhmALTV  48169