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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3890  {copab 5148   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-opab 5149  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  7468  oprres  7528  fimaproj  8078  xpord2pred  8088  xpord3pred  8095  naddcllem  8605  naddov2  8608  naddunif  8622  naddasslem1  8623  naddasslem2  8624  pmss12g  8810  marypha1lem  9339  marypha2lem1  9341  hartogslem1  9450  infxpenlem  9926  dfac5lem4  10039  dfac5lem4OLD  10041  axdc4lem  10368  fpwwe2lem1  10545  fpwwe2lem10  10554  fpwwe2lem11  10555  fpwwe2lem12  10556  canthwe  10565  tskxpss  10686  dmaddpi  10804  dmmulpi  10805  addnqf  10862  mulnqf  10863  rexpssxrxp  11181  ltrelxr  11197  mulnzcnf  11787  dfz2  12534  elq  12891  leiso  14412  znnen  16170  phimullem  16740  imasless  17495  sscpwex  17773  fullsubc  17808  fullresc  17809  wunfunc  17859  funcres2c  17861  homaf  17988  dmcoass  18024  catcoppccl  18075  catcfuccl  18076  catcxpccl  18164  rnghmresfn  20587  rnghmsscmap2  20597  rnghmsscmap  20598  rhmresfn  20616  rhmsscmap2  20626  rhmsscmap  20627  rhmsscrnghm  20633  rngcrescrhm  20652  znleval  21544  txuni2  23540  txbas  23542  txcld  23578  txcls  23579  neitx  23582  txcnp  23595  txlly  23611  txnlly  23612  hausdiag  23620  tx1stc  23625  txkgen  23627  xkococnlem  23634  cnmpt2res  23652  clssubg  24084  tsmsxplem1  24128  tsmsxplem2  24129  tsmsxp  24130  trust  24204  ustuqtop1  24216  psmetres2  24289  xmetres2  24336  metres2  24338  ressprdsds  24346  xmetresbl  24412  ressxms  24500  metustexhalf  24531  cfilucfil  24534  restmetu  24545  nrginvrcn  24667  qtopbaslem  24733  tgqioo  24775  re2ndc  24776  resubmet  24777  xrsdsre  24786  bndth  24935  lebnumii  24943  iscfil2  25243  cmssmscld  25327  cmsss  25328  cmscsscms  25350  minveclem3a  25404  ovolfsf  25448  opnmblALT  25580  mbfimaopnlem  25632  itg1addlem4  25676  limccnp2  25869  taylfval  26335  taylf  26337  mpodvdsmulf1o  27171  fsumdvdsmul  27172  dvdsmulf1o  27173  elzs  28390  sspg  30814  ssps  30816  sspmlem  30818  issh2  31295  hhssabloilem  31347  hhssabloi  31348  hhssnv  31350  hhshsslem1  31353  shsel  31400  iunxpssiun1  32653  ofrn2  32728  djussxp2  32736  gtiso  32789  xrofsup  32855  gsumwrd2dccatlem  33153  txomap  33994  tpr2rico  34072  prsss  34076  raddcn  34089  xrge0pluscn  34100  br2base  34429  dya2iocnrect  34441  dya2iocucvr  34444  eulerpartlemgh  34538  eulerpartlemgs2  34540  cvmlift2lem9  35509  cvmlift2lem10  35510  cvmlift2lem11  35511  cvmlift2lem12  35512  mpstssv  35737  elxp8  37701  mblfinlem2  37993  ftc1anc  38036  ssbnd  38123  prdsbnd2  38130  cnpwstotbnd  38132  reheibor  38174  exidreslem  38212  divrngcl  38292  isdrngo2  38293  dibss  41629  xppss12  42684  arearect  43661  rtrclex  44062  rtrclexi  44066  rr2sscn2  45813  fourierdlem42  46595  opnvonmbllem2  47079  rngcrescrhmALTV  48768  imaidfu  49597  imasubc  49638