Theorem xpss12 5656

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3917  {copab 5172   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-opab 5173  df-xp 5647

This theorem is referenced by:  xpss  5657  inxpssres  5658  xpss1  5660  xpss2  5661  djussxp  5812  ssxpb  6150  resssxp  6246  cossxp  6248  relrelss  6249  fssxp  6718  oprabss  7500  oprres  7560  fimaproj  8117  xpord2pred  8127  xpord3pred  8134  naddcllem  8643  naddov2  8646  naddunif  8660  naddasslem1  8661  naddasslem2  8662  pmss12g  8845  marypha1lem  9391  marypha2lem1  9393  hartogslem1  9502  infxpenlem  9973  dfac5lem4  10086  dfac5lem4OLD  10088  axdc4lem  10415  fpwwe2lem1  10591  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2lem12  10602  canthwe  10611  tskxpss  10732  dmaddpi  10850  dmmulpi  10851  addnqf  10908  mulnqf  10909  rexpssxrxp  11226  ltrelxr  11242  mulnzcnf  11831  dfz2  12555  elq  12916  leiso  14431  znnen  16187  phimullem  16756  imasless  17510  sscpwex  17784  fullsubc  17819  fullresc  17820  wunfunc  17870  funcres2c  17872  homaf  17999  dmcoass  18035  catcoppccl  18086  catcfuccl  18087  catcxpccl  18175  rnghmresfn  20535  rnghmsscmap2  20545  rnghmsscmap  20546  rhmresfn  20564  rhmsscmap2  20574  rhmsscmap  20575  rhmsscrnghm  20581  rngcrescrhm  20600  znleval  21471  txuni2  23459  txbas  23461  txcld  23497  txcls  23498  neitx  23501  txcnp  23514  txlly  23530  txnlly  23531  hausdiag  23539  tx1stc  23544  txkgen  23546  xkococnlem  23553  cnmpt2res  23571  clssubg  24003  tsmsxplem1  24047  tsmsxplem2  24048  tsmsxp  24049  trust  24124  ustuqtop1  24136  psmetres2  24209  xmetres2  24256  metres2  24258  ressprdsds  24266  xmetresbl  24332  ressxms  24420  metustexhalf  24451  cfilucfil  24454  restmetu  24465  nrginvrcn  24587  qtopbaslem  24653  tgqioo  24695  re2ndc  24696  resubmet  24697  xrsdsre  24706  bndth  24864  lebnumii  24872  iscfil2  25173  cmssmscld  25257  cmsss  25258  cmscsscms  25280  minveclem3a  25334  ovolfsf  25379  opnmblALT  25511  mbfimaopnlem  25563  itg1addlem4  25607  limccnp2  25800  taylfval  26273  taylf  26275  mpodvdsmulf1o  27111  fsumdvdsmul  27112  dvdsmulf1o  27113  fsumdvdsmulOLD  27114  elzs  28279  sspg  30664  ssps  30666  sspmlem  30668  issh2  31145  hhssabloilem  31197  hhssabloi  31198  hhssnv  31200  hhshsslem1  31203  shsel  31250  iunxpssiun1  32504  ofrn2  32571  djussxp2  32579  gtiso  32631  xrofsup  32697  gsumwrd2dccatlem  33013  txomap  33831  tpr2rico  33909  prsss  33913  raddcn  33926  xrge0pluscn  33937  br2base  34267  dya2iocnrect  34279  dya2iocucvr  34282  eulerpartlemgh  34376  eulerpartlemgs2  34378  cvmlift2lem9  35305  cvmlift2lem10  35306  cvmlift2lem11  35307  cvmlift2lem12  35308  mpstssv  35533  elxp8  37366  mblfinlem2  37659  ftc1anc  37702  ssbnd  37789  prdsbnd2  37796  cnpwstotbnd  37798  reheibor  37840  exidreslem  37878  divrngcl  37958  isdrngo2  37959  dibss  41170  xppss12  42224  arearect  43211  rtrclex  43613  rtrclexi  43617  rr2sscn2  45369  fourierdlem42  46154  opnvonmbllem2  46638  rngcrescrhmALTV  48272  imaidfu  49103  imasubc  49144