Theorem xpss12 5660

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   ⊆ wss 3904  {copab 5161   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3921  df-opab 5162  df-xp 5651

This theorem is referenced by:  xpss  5661  inxpssres  5662  xpss1  5664  xpss2  5665  djussxp  5815  ssxpb  6156  resssxp  6253  cossxp  6255  relrelss  6256  fssxp  6715  oprabss  7500  oprres  7560  fimaproj  8110  xpord2pred  8120  xpord3pred  8127  naddcllem  8641  naddov2  8644  naddunif  8659  naddasslem1  8660  naddasslem2  8661  pmss12g  8847  marypha1lem  9376  marypha2lem1  9378  hartogslem1  9487  infxpenlem  9966  dfac5lem4  10079  dfac5lem4OLD  10081  axdc4lem  10409  fpwwe2lem1  10586  fpwwe2lem10  10595  fpwwe2lem11  10596  fpwwe2lem12  10597  canthwe  10606  tskxpss  10727  dmaddpi  10845  dmmulpi  10846  addnqf  10903  mulnqf  10904  rexpssxrxp  11224  ltrelxr  11240  mulnzcnf  11830  dfz2  12584  elq  12948  leiso  14469  znnen  16227  phimullem  16797  imasless  17553  sscpwex  17831  fullsubc  17866  fullresc  17867  wunfunc  17917  funcres2c  17919  homaf  18046  dmcoass  18082  catcoppccl  18133  catcfuccl  18134  catcxpccl  18222  rnghmresfn  20648  rnghmsscmap2  20658  rnghmsscmap  20659  rhmresfn  20677  rhmsscmap2  20687  rhmsscmap  20688  rhmsscrnghm  20694  rngcrescrhm  20713  znleval  21586  txuni2  23605  txbas  23607  txcld  23643  txcls  23644  neitx  23647  txcnp  23660  txlly  23676  txnlly  23677  hausdiag  23685  tx1stc  23690  txkgen  23692  xkococnlem  23699  cnmpt2res  23717  clssubg  24149  tsmsxplem1  24193  tsmsxplem2  24194  tsmsxp  24195  trust  24269  ustuqtop1  24281  psmetres2  24354  xmetres2  24401  metres2  24403  ressprdsds  24411  xmetresbl  24477  ressxms  24565  metustexhalf  24596  cfilucfil  24599  restmetu  24610  nrginvrcn  24732  qtopbaslem  24798  tgqioo  24840  re2ndc  24841  resubmet  24842  xrsdsre  24851  bndth  25000  lebnumii  25008  iscfil2  25308  cmssmscld  25392  cmsss  25393  cmscsscms  25415  minveclem3a  25469  ovolfsf  25513  opnmblALT  25645  mbfimaopnlem  25697  itg1addlem4  25741  limccnp2  25934  taylfval  26399  taylf  26401  mpodvdsmulf1o  27235  fsumdvdsmul  27236  dvdsmulf1o  27237  elzs  28454  sspg  30877  ssps  30879  sspmlem  30881  issh2  31358  hhssabloilem  31410  hhssabloi  31411  hhssnv  31413  hhshsslem1  31416  shsel  31463  iunxpssiun1  32717  ofrn2  32792  djussxp2  32800  gtiso  32853  xrofsup  32919  gsumwrd2dccatlem  33218  txomap  34092  tpr2rico  34170  prsss  34174  raddcn  34187  xrge0pluscn  34198  br2base  34527  dya2iocnrect  34539  dya2iocucvr  34542  eulerpartlemgh  34636  eulerpartlemgs2  34638  cvmlift2lem9  35625  cvmlift2lem10  35626  cvmlift2lem11  35627  cvmlift2lem12  35628  mpstssv  35853  nmulprop  36504  elxp8  37829  mblfinlem2  38121  ftc1anc  38164  ssbnd  38251  prdsbnd2  38258  cnpwstotbnd  38260  reheibor  38302  exidreslem  38340  divrngcl  38420  isdrngo2  38421  dibss  41757  xppss12  42812  arearect  43756  rtrclex  44157  rtrclexi  44161  rr2sscn2  45905  fourierdlem42  46687  opnvonmbllem2  47171  rngcrescrhmALTV  48866  imaidfu  49695  imasubc  49736