Theorem xpss12 5667

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145   ⊆ wss 3907  {copab 5167   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3924  df-opab 5168  df-xp 5658

This theorem is referenced by:  xpss  5668  inxpssres  5669  xpss1  5671  xpss2  5672  djussxp  5822  ssxpb  6164  resssxp  6261  cossxp  6263  relrelss  6264  fssxp  6723  oprabss  7508  oprres  7568  fimaproj  8119  xpord2pred  8129  xpord3pred  8136  naddcllem  8650  naddov2  8653  naddunif  8668  naddasslem1  8669  naddasslem2  8670  pmss12g  8855  marypha1lem  9381  marypha2lem1  9383  hartogslem1  9492  infxpenlem  9985  dfac5lem4  10098  axdc4lem  10427  fpwwe2lem1  10604  fpwwe2lem10  10613  fpwwe2lem11  10614  fpwwe2lem12  10615  canthwe  10624  tskxpss  10745  dmaddpi  10863  dmmulpi  10864  addnqf  10921  mulnqf  10922  rexpssxrxp  11242  ltrelxr  11258  mulnzcnf  11848  dfz2  12601  elq  12965  leiso  14486  znnen  16258  phimullem  16828  imasless  17584  sscpwex  17862  fullsubc  17897  fullresc  17898  wunfunc  17948  funcres2c  17950  homaf  18077  dmcoass  18113  catcoppccl  18164  catcfuccl  18165  catcxpccl  18253  rnghmresfn  20695  rnghmsscmap2  20705  rnghmsscmap  20706  rhmresfn  20724  rhmsscmap2  20734  rhmsscmap  20735  rhmsscrnghm  20741  rngcrescrhm  20760  znleval  21664  txuni2  23683  txbas  23685  txcld  23721  txcls  23722  neitx  23725  txcnp  23738  txlly  23754  txnlly  23755  hausdiag  23763  tx1stc  23768  txkgen  23770  xkococnlem  23777  cnmpt2res  23795  clssubg  24227  tsmsxplem1  24271  tsmsxplem2  24272  tsmsxp  24273  trust  24347  ustuqtop1  24359  psmetres2  24432  xmetres2  24479  metres2  24481  ressprdsds  24489  xmetresbl  24555  ressxms  24643  metustexhalf  24674  cfilucfil  24677  restmetu  24688  nrginvrcn  24810  qtopbaslem  24876  tgqioo  24918  re2ndc  24919  resubmet  24920  xrsdsre  24929  bndth  25078  lebnumii  25086  iscfil2  25386  cmssmscld  25470  cmsss  25471  cmscsscms  25493  minveclem3a  25547  ovolfsf  25591  opnmblALT  25723  mbfimaopnlem  25775  itg1addlem4  25819  limccnp2  26012  taylfval  26480  taylf  26482  mpodvdsmulf1o  27316  fsumdvdsmul  27317  dvdsmulf1o  27318  elzs  28535  sspg  30989  ssps  30991  sspmlem  30993  issh2  31470  hhssabloilem  31522  hhssabloi  31523  hhssnv  31525  hhshsslem1  31528  shsel  31575  iunxpssiun1  32823  ofrn2  32897  djussxp2  32905  gtiso  32958  xrofsup  33024  gsumwrd2dccatlem  33310  txomap  34141  tpr2rico  34219  prsss  34223  raddcn  34236  xrge0pluscn  34247  br2base  34576  dya2iocnrect  34588  dya2iocucvr  34591  eulerpartlemgh  34685  eulerpartlemgs2  34687  cvmlift2lem9  35674  cvmlift2lem10  35675  cvmlift2lem11  35676  cvmlift2lem12  35677  mpstssv  35902  nmulprop  36553  elxp8  37877  mblfinlem2  38169  ftc1anc  38212  ssbnd  38299  prdsbnd2  38306  cnpwstotbnd  38308  reheibor  38350  exidreslem  38388  divrngcl  38468  isdrngo2  38469  dibss  41805  xppss12  42860  arearect  43804  rtrclex  44205  rtrclexi  44209  rr2sscn2  45939  fourierdlem42  46721  opnvonmbllem2  47205  rngcrescrhmALTV  48900  imaidfu  49739  imasubc  49780