Theorem xpss12 5653

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3914  {copab 5169   × cxp 5636

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-opab 5170  df-xp 5644

This theorem is referenced by:  xpss  5654  inxpssres  5655  xpss1  5657  xpss2  5658  djussxp  5809  ssxpb  6147  resssxp  6243  cossxp  6245  relrelss  6246  fssxp  6715  oprabss  7497  oprres  7557  fimaproj  8114  xpord2pred  8124  xpord3pred  8131  naddcllem  8640  naddov2  8643  naddunif  8657  naddasslem1  8658  naddasslem2  8659  pmss12g  8842  marypha1lem  9384  marypha2lem1  9386  hartogslem1  9495  infxpenlem  9966  dfac5lem4  10079  dfac5lem4OLD  10081  axdc4lem  10408  fpwwe2lem1  10584  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2lem12  10595  canthwe  10604  tskxpss  10725  dmaddpi  10843  dmmulpi  10844  addnqf  10901  mulnqf  10902  rexpssxrxp  11219  ltrelxr  11235  mulnzcnf  11824  dfz2  12548  elq  12909  leiso  14424  znnen  16180  phimullem  16749  imasless  17503  sscpwex  17777  fullsubc  17812  fullresc  17813  wunfunc  17863  funcres2c  17865  homaf  17992  dmcoass  18028  catcoppccl  18079  catcfuccl  18080  catcxpccl  18168  rnghmresfn  20528  rnghmsscmap2  20538  rnghmsscmap  20539  rhmresfn  20557  rhmsscmap2  20567  rhmsscmap  20568  rhmsscrnghm  20574  rngcrescrhm  20593  znleval  21464  txuni2  23452  txbas  23454  txcld  23490  txcls  23491  neitx  23494  txcnp  23507  txlly  23523  txnlly  23524  hausdiag  23532  tx1stc  23537  txkgen  23539  xkococnlem  23546  cnmpt2res  23564  clssubg  23996  tsmsxplem1  24040  tsmsxplem2  24041  tsmsxp  24042  trust  24117  ustuqtop1  24129  psmetres2  24202  xmetres2  24249  metres2  24251  ressprdsds  24259  xmetresbl  24325  ressxms  24413  metustexhalf  24444  cfilucfil  24447  restmetu  24458  nrginvrcn  24580  qtopbaslem  24646  tgqioo  24688  re2ndc  24689  resubmet  24690  xrsdsre  24699  bndth  24857  lebnumii  24865  iscfil2  25166  cmssmscld  25250  cmsss  25251  cmscsscms  25273  minveclem3a  25327  ovolfsf  25372  opnmblALT  25504  mbfimaopnlem  25556  itg1addlem4  25600  limccnp2  25793  taylfval  26266  taylf  26268  mpodvdsmulf1o  27104  fsumdvdsmul  27105  dvdsmulf1o  27106  fsumdvdsmulOLD  27107  elzs  28272  sspg  30657  ssps  30659  sspmlem  30661  issh2  31138  hhssabloilem  31190  hhssabloi  31191  hhssnv  31193  hhshsslem1  31196  shsel  31243  iunxpssiun1  32497  ofrn2  32564  djussxp2  32572  gtiso  32624  xrofsup  32690  gsumwrd2dccatlem  33006  txomap  33824  tpr2rico  33902  prsss  33906  raddcn  33919  xrge0pluscn  33930  br2base  34260  dya2iocnrect  34272  dya2iocucvr  34275  eulerpartlemgh  34369  eulerpartlemgs2  34371  cvmlift2lem9  35298  cvmlift2lem10  35299  cvmlift2lem11  35300  cvmlift2lem12  35301  mpstssv  35526  elxp8  37359  mblfinlem2  37652  ftc1anc  37695  ssbnd  37782  prdsbnd2  37789  cnpwstotbnd  37791  reheibor  37833  exidreslem  37871  divrngcl  37951  isdrngo2  37952  dibss  41163  xppss12  42217  arearect  43204  rtrclex  43606  rtrclexi  43610  rr2sscn2  45362  fourierdlem42  46147  opnvonmbllem2  46631  rngcrescrhmALTV  48268  imaidfu  49099  imasubc  49140