Theorem xpss12 5700

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3951  {copab 5205   × cxp 5683

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-opab 5206  df-xp 5691

This theorem is referenced by:  xpss  5701  inxpssres  5702  xpss1  5704  xpss2  5705  djussxp  5856  ssxpb  6194  resssxp  6290  cossxp  6292  relrelss  6293  fssxp  6763  oprabss  7541  oprres  7601  fimaproj  8160  xpord2pred  8170  xpord3pred  8177  naddcllem  8714  naddov2  8717  naddunif  8731  naddasslem1  8732  naddasslem2  8733  pmss12g  8909  marypha1lem  9473  marypha2lem1  9475  hartogslem1  9582  infxpenlem  10053  dfac5lem4  10166  dfac5lem4OLD  10168  axdc4lem  10495  fpwwe2lem1  10671  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  canthwe  10691  tskxpss  10812  dmaddpi  10930  dmmulpi  10931  addnqf  10988  mulnqf  10989  rexpssxrxp  11306  ltrelxr  11322  mulnzcnf  11909  dfz2  12632  elq  12992  leiso  14498  znnen  16248  phimullem  16816  imasless  17585  sscpwex  17859  fullsubc  17895  fullresc  17896  wunfunc  17946  funcres2c  17948  homaf  18075  dmcoass  18111  catcoppccl  18162  catcfuccl  18163  catcxpccl  18252  rnghmresfn  20619  rnghmsscmap2  20629  rnghmsscmap  20630  rhmresfn  20648  rhmsscmap2  20658  rhmsscmap  20659  rhmsscrnghm  20665  rngcrescrhm  20684  znleval  21573  txuni2  23573  txbas  23575  txcld  23611  txcls  23612  neitx  23615  txcnp  23628  txlly  23644  txnlly  23645  hausdiag  23653  tx1stc  23658  txkgen  23660  xkococnlem  23667  cnmpt2res  23685  clssubg  24117  tsmsxplem1  24161  tsmsxplem2  24162  tsmsxp  24163  trust  24238  ustuqtop1  24250  psmetres2  24324  xmetres2  24371  metres2  24373  ressprdsds  24381  xmetresbl  24447  ressxms  24538  metustexhalf  24569  cfilucfil  24572  restmetu  24583  nrginvrcn  24713  qtopbaslem  24779  tgqioo  24821  re2ndc  24822  resubmet  24823  xrsdsre  24832  bndth  24990  lebnumii  24998  iscfil2  25300  cmssmscld  25384  cmsss  25385  cmscsscms  25407  minveclem3a  25461  ovolfsf  25506  opnmblALT  25638  mbfimaopnlem  25690  itg1addlem4  25734  limccnp2  25927  taylfval  26400  taylf  26402  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  elzs  28370  sspg  30747  ssps  30749  sspmlem  30751  issh2  31228  hhssabloilem  31280  hhssabloi  31281  hhssnv  31283  hhshsslem1  31286  shsel  31333  iunxpssiun1  32581  ofrn2  32650  djussxp2  32658  gtiso  32710  xrofsup  32771  gsumwrd2dccatlem  33069  txomap  33833  tpr2rico  33911  prsss  33915  raddcn  33928  xrge0pluscn  33939  br2base  34271  dya2iocnrect  34283  dya2iocucvr  34286  eulerpartlemgh  34380  eulerpartlemgs2  34382  cvmlift2lem9  35316  cvmlift2lem10  35317  cvmlift2lem11  35318  cvmlift2lem12  35319  mpstssv  35544  elxp8  37372  mblfinlem2  37665  ftc1anc  37708  ssbnd  37795  prdsbnd2  37802  cnpwstotbnd  37804  reheibor  37846  exidreslem  37884  divrngcl  37964  isdrngo2  37965  dibss  41171  xppss12  42268  arearect  43227  rtrclex  43630  rtrclexi  43634  rr2sscn2  45377  fourierdlem42  46164  opnvonmbllem2  46648  rngcrescrhmALTV  48196