Theorem xpss12 5682

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098   ⊆ wss 3941  {copab 5201   × cxp 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3948  df-ss 3958  df-opab 5202  df-xp 5673

This theorem is referenced by:  xpss  5683  inxpssres  5684  xpss1  5686  xpss2  5687  djussxp  5836  ssxpb  6164  resssxp  6260  cossxp  6262  relrelss  6263  fssxp  6736  oprabss  7508  oprres  7569  fimaproj  8116  xpord2pred  8126  xpord3pred  8133  naddcllem  8672  naddov2  8675  naddunif  8689  naddasslem1  8690  naddasslem2  8691  pmss12g  8860  marypha1lem  9425  marypha2lem1  9427  hartogslem1  9534  infxpenlem  10005  dfac5lem4  10118  axdc4lem  10447  fpwwe2lem1  10623  fpwwe2lem10  10632  fpwwe2lem11  10633  fpwwe2lem12  10634  canthwe  10643  tskxpss  10764  dmaddpi  10882  dmmulpi  10883  addnqf  10940  mulnqf  10941  rexpssxrxp  11257  ltrelxr  11273  mulnzcnf  11858  dfz2  12575  elq  12932  leiso  14418  znnen  16154  phimullem  16713  imasless  17487  sscpwex  17763  fullsubc  17801  fullresc  17802  wunfunc  17852  wunfuncOLD  17853  funcres2c  17855  homaf  17984  dmcoass  18020  catcoppccl  18071  catcoppcclOLD  18072  catcfuccl  18073  catcfucclOLD  18074  catcxpccl  18163  catcxpcclOLD  18164  rnghmresfn  20507  rnghmsscmap2  20517  rnghmsscmap  20518  rhmresfn  20536  rhmsscmap2  20546  rhmsscmap  20547  rhmsscrnghm  20553  rngcrescrhm  20572  znleval  21419  txuni2  23393  txbas  23395  txcld  23431  txcls  23432  neitx  23435  txcnp  23448  txlly  23464  txnlly  23465  hausdiag  23473  tx1stc  23478  txkgen  23480  xkococnlem  23487  cnmpt2res  23505  clssubg  23937  tsmsxplem1  23981  tsmsxplem2  23982  tsmsxp  23983  trust  24058  ustuqtop1  24070  psmetres2  24144  xmetres2  24191  metres2  24193  ressprdsds  24201  xmetresbl  24267  ressxms  24358  metustexhalf  24389  cfilucfil  24392  restmetu  24403  nrginvrcn  24533  qtopbaslem  24599  tgqioo  24640  re2ndc  24641  resubmet  24642  xrsdsre  24650  bndth  24808  lebnumii  24816  iscfil2  25118  cmssmscld  25202  cmsss  25203  cmscsscms  25225  minveclem3a  25279  ovolfsf  25324  opnmblALT  25456  mbfimaopnlem  25508  itg1addlem4  25552  itg1addlem4OLD  25553  limccnp2  25745  taylfval  26214  taylf  26216  mpodvdsmulf1o  27045  fsumdvdsmul  27046  dvdsmulf1o  27047  fsumdvdsmulOLD  27048  sspg  30453  ssps  30455  sspmlem  30457  issh2  30934  hhssabloilem  30986  hhssabloi  30987  hhssnv  30989  hhshsslem1  30992  shsel  31039  ofrn2  32337  djussxp2  32345  gtiso  32394  xrofsup  32452  txomap  33306  tpr2rico  33384  prsss  33388  raddcn  33401  xrge0pluscn  33412  br2base  33760  dya2iocnrect  33772  dya2iocucvr  33775  eulerpartlemgh  33869  eulerpartlemgs2  33871  cvmlift2lem9  34793  cvmlift2lem10  34794  cvmlift2lem11  34795  cvmlift2lem12  34796  mpstssv  35021  elxp8  36743  mblfinlem2  37020  ftc1anc  37063  ssbnd  37150  prdsbnd2  37157  cnpwstotbnd  37159  reheibor  37201  exidreslem  37239  divrngcl  37319  isdrngo2  37320  dibss  40534  xppss12  41544  arearect  42478  rtrclex  42882  rtrclexi  42886  rr2sscn2  44586  fourierdlem42  45375  opnvonmbllem2  45859  rngcrescrhmALTV  47168