Theorem xpss12 5604

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3887  {copab 5136   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595

This theorem is referenced by:  xpss  5605  inxpssres  5606  xpss1  5608  xpss2  5609  djussxp  5754  ssxpb  6077  resssxp  6173  cossxp  6175  relrelss  6176  fssxp  6628  oprabss  7381  oprres  7440  fimaproj  7976  pmss12g  8657  marypha1lem  9192  marypha2lem1  9194  hartogslem1  9301  infxpenlem  9769  dfac5lem4  9882  axdc4lem  10211  fpwwe2lem1  10387  fpwwe2lem10  10396  fpwwe2lem11  10397  fpwwe2lem12  10398  canthwe  10407  tskxpss  10528  dmaddpi  10646  dmmulpi  10647  addnqf  10704  mulnqf  10705  rexpssxrxp  11020  ltrelxr  11036  mulnzcnopr  11621  dfz2  12338  elq  12690  leiso  14173  znnen  15921  phimullem  16480  imasless  17251  sscpwex  17527  fullsubc  17565  fullresc  17566  wunfunc  17614  wunfuncOLD  17615  funcres2c  17617  homaf  17745  dmcoass  17781  catcoppccl  17832  catcoppcclOLD  17833  catcfuccl  17834  catcfucclOLD  17835  catcxpccl  17924  catcxpcclOLD  17925  znleval  20762  txuni2  22716  txbas  22718  txcld  22754  txcls  22755  neitx  22758  txcnp  22771  txlly  22787  txnlly  22788  hausdiag  22796  tx1stc  22801  txkgen  22803  xkococnlem  22810  cnmpt2res  22828  clssubg  23260  tsmsxplem1  23304  tsmsxplem2  23305  tsmsxp  23306  trust  23381  ustuqtop1  23393  psmetres2  23467  xmetres2  23514  metres2  23516  ressprdsds  23524  xmetresbl  23590  ressxms  23681  metustexhalf  23712  cfilucfil  23715  restmetu  23726  nrginvrcn  23856  qtopbaslem  23922  tgqioo  23963  re2ndc  23964  resubmet  23965  xrsdsre  23973  bndth  24121  lebnumii  24129  iscfil2  24430  cmssmscld  24514  cmsss  24515  cmscsscms  24537  minveclem3a  24591  ovolfsf  24635  opnmblALT  24767  mbfimaopnlem  24819  itg1addlem4  24863  itg1addlem4OLD  24864  limccnp2  25056  taylfval  25518  taylf  25520  dvdsmulf1o  26343  fsumdvdsmul  26344  sspg  29090  ssps  29092  sspmlem  29094  issh2  29571  hhssabloilem  29623  hhssabloi  29624  hhssnv  29626  hhshsslem1  29629  shsel  29676  ofrn2  30977  djussxp2  30985  gtiso  31033  xrofsup  31090  txomap  31784  tpr2rico  31862  prsss  31866  raddcn  31879  xrge0pluscn  31890  br2base  32236  dya2iocnrect  32248  dya2iocucvr  32251  eulerpartlemgh  32345  eulerpartlemgs2  32347  cvmlift2lem9  33273  cvmlift2lem10  33274  cvmlift2lem11  33275  cvmlift2lem12  33276  mpstssv  33501  xpord2pred  33792  xpord3pred  33798  naddcllem  33831  naddov2  33834  addscllem1  34131  elxp8  35542  mblfinlem2  35815  ftc1anc  35858  ssbnd  35946  prdsbnd2  35953  cnpwstotbnd  35955  reheibor  35997  exidreslem  36035  divrngcl  36115  isdrngo2  36116  dibss  39183  xppss12  40204  arearect  41046  rtrclex  41225  rtrclexi  41229  rr2sscn2  42905  fourierdlem42  43690  opnvonmbllem2  44171  rnghmresfn  45521  rnghmsscmap2  45531  rnghmsscmap  45532  rhmresfn  45567  rhmsscmap2  45577  rhmsscmap  45578  rhmsscrnghm  45584  rngcrescrhm  45643  rngcrescrhmALTV  45661