Theorem xpss12 5669

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3926  {copab 5181   × cxp 5652

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-opab 5182  df-xp 5660

This theorem is referenced by:  xpss  5670  inxpssres  5671  xpss1  5673  xpss2  5674  djussxp  5825  ssxpb  6163  resssxp  6259  cossxp  6261  relrelss  6262  fssxp  6732  oprabss  7513  oprres  7573  fimaproj  8132  xpord2pred  8142  xpord3pred  8149  naddcllem  8686  naddov2  8689  naddunif  8703  naddasslem1  8704  naddasslem2  8705  pmss12g  8881  marypha1lem  9443  marypha2lem1  9445  hartogslem1  9554  infxpenlem  10025  dfac5lem4  10138  dfac5lem4OLD  10140  axdc4lem  10467  fpwwe2lem1  10643  fpwwe2lem10  10652  fpwwe2lem11  10653  fpwwe2lem12  10654  canthwe  10663  tskxpss  10784  dmaddpi  10902  dmmulpi  10903  addnqf  10960  mulnqf  10961  rexpssxrxp  11278  ltrelxr  11294  mulnzcnf  11881  dfz2  12605  elq  12964  leiso  14475  znnen  16228  phimullem  16796  imasless  17552  sscpwex  17826  fullsubc  17861  fullresc  17862  wunfunc  17912  funcres2c  17914  homaf  18041  dmcoass  18077  catcoppccl  18128  catcfuccl  18129  catcxpccl  18217  rnghmresfn  20577  rnghmsscmap2  20587  rnghmsscmap  20588  rhmresfn  20606  rhmsscmap2  20616  rhmsscmap  20617  rhmsscrnghm  20623  rngcrescrhm  20642  znleval  21513  txuni2  23501  txbas  23503  txcld  23539  txcls  23540  neitx  23543  txcnp  23556  txlly  23572  txnlly  23573  hausdiag  23581  tx1stc  23586  txkgen  23588  xkococnlem  23595  cnmpt2res  23613  clssubg  24045  tsmsxplem1  24089  tsmsxplem2  24090  tsmsxp  24091  trust  24166  ustuqtop1  24178  psmetres2  24251  xmetres2  24298  metres2  24300  ressprdsds  24308  xmetresbl  24374  ressxms  24462  metustexhalf  24493  cfilucfil  24496  restmetu  24507  nrginvrcn  24629  qtopbaslem  24695  tgqioo  24737  re2ndc  24738  resubmet  24739  xrsdsre  24748  bndth  24906  lebnumii  24914  iscfil2  25216  cmssmscld  25300  cmsss  25301  cmscsscms  25323  minveclem3a  25377  ovolfsf  25422  opnmblALT  25554  mbfimaopnlem  25606  itg1addlem4  25650  limccnp2  25843  taylfval  26316  taylf  26318  mpodvdsmulf1o  27154  fsumdvdsmul  27155  dvdsmulf1o  27156  fsumdvdsmulOLD  27157  elzs  28287  sspg  30655  ssps  30657  sspmlem  30659  issh2  31136  hhssabloilem  31188  hhssabloi  31189  hhssnv  31191  hhshsslem1  31194  shsel  31241  iunxpssiun1  32495  ofrn2  32564  djussxp2  32572  gtiso  32624  xrofsup  32690  gsumwrd2dccatlem  33006  txomap  33811  tpr2rico  33889  prsss  33893  raddcn  33906  xrge0pluscn  33917  br2base  34247  dya2iocnrect  34259  dya2iocucvr  34262  eulerpartlemgh  34356  eulerpartlemgs2  34358  cvmlift2lem9  35279  cvmlift2lem10  35280  cvmlift2lem11  35281  cvmlift2lem12  35282  mpstssv  35507  elxp8  37335  mblfinlem2  37628  ftc1anc  37671  ssbnd  37758  prdsbnd2  37765  cnpwstotbnd  37767  reheibor  37809  exidreslem  37847  divrngcl  37927  isdrngo2  37928  dibss  41134  xppss12  42226  arearect  43186  rtrclex  43588  rtrclexi  43592  rr2sscn2  45341  fourierdlem42  46126  opnvonmbllem2  46610  rngcrescrhmALTV  48203  imaidfu  49017  imasubc  49039