Theorem xpss12 5674

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ⊆ wss 3902  {copab 5171   × cxp 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-opab 5172  df-xp 5665

This theorem is used by:  xpss  5675  inxpssres  5676  xpss1  5678  xpss2  5679  djussxp  5829  ssxpb  6171  resssxp  6271  cossxp  6273  relrelss  6274  fssxp  6734  oprabss  7525  oprres  7585  fimaproj  8137  xpord2pred  8147  xpord3pred  8154  naddcllem  8668  naddov2  8671  naddunif  8686  naddasslem1  8687  naddasslem2  8688  pmss12g  8880  marypha1lem  9407  marypha2lem1  9409  hartogslem1  9518  infxpenlem  10020  dfac5lem4  10133  axdc4lem  10461  fpwwe2lem1  10644  fpwwe2lem10  10653  fpwwe2lem11  10654  fpwwe2lem12  10655  canthwe  10664  tskxpss  10785  dmaddpi  10903  dmmulpi  10904  addnqf  10961  mulnqf  10962  rexpssxrxp  11282  ltrelxr  11298  mulnzcnf  11888  dfz2  12638  elq  13003  leiso  14528  znnen  16306  phimullem  16876  imasless  17632  sscpwex  17910  fullsubc  17945  fullresc  17946  wunfunc  17996  funcres2c  17998  homaf  18125  dmcoass  18161  catcoppccl  18212  catcfuccl  18213  catcxpccl  18301  rnghmresfn  20787  rnghmsscmap2  20797  rnghmsscmap  20798  rhmresfn  20816  rhmsscmap2  20826  rhmsscmap  20827  rhmsscrnghm  20833  rngcrescrhm  20852  znleval  21773  txuni2  23797  txbas  23799  txcld  23835  txcls  23836  neitx  23839  txcnp  23852  txlly  23868  txnlly  23869  hausdiag  23877  tx1stc  23882  txkgen  23884  xkococnlem  23891  cnmpt2res  23909  clssubg  24341  tsmsxplem1  24385  tsmsxplem2  24386  tsmsxp  24387  trust  24461  ustuqtop1  24473  psmetres2  24546  xmetres2  24593  metres2  24595  ressprdsds  24603  xmetresbl  24669  ressxms  24757  metustexhalf  24788  cfilucfil  24791  restmetu  24802  nrginvrcn  24924  qtopbaslem  24990  tgqioo  25032  re2ndc  25033  resubmet  25034  xrsdsre  25043  bndth  25192  lebnumii  25200  iscfil2  25500  cmssmscld  25584  cmsss  25585  cmscsscms  25607  minveclem3a  25661  ovolfsf  25705  opnmblALT  25837  mbfimaopnlem  25889  itg1addlem4  25933  limccnp2  26126  taylfval  26602  taylf  26604  mpodvdsmulf1o  27438  fsumdvdsmul  27439  dvdsmulf1o  27440  elzs  28657  sspg  31217  ssps  31219  sspmlem  31221  issh2  31698  hhssabloilem  31750  hhssabloi  31751  hhssnv  31753  hhshsslem1  31756  shsel  31803  iunxpssiun1  33049  ofrn2  33121  djussxp2  33129  gtiso  33181  xrofsup  33246  gsumwrd2dccatlem  33525  txomap  34352  tpr2rico  34430  prsss  34434  raddcn  34447  xrge0pluscn  34458  br2base  34788  dya2iocnrect  34800  dya2iocucvr  34803  eulerpartlemgh  34897  eulerpartlemgs2  34899  cvmlift2lem9  35898  cvmlift2lem10  35899  cvmlift2lem11  35900  cvmlift2lem12  35901  mpstssv  36126  nmulprop  36778  elxp8  38133  mblfinlem2  38415  ftc1anc  38458  ssbnd  38546  prdsbnd2  38553  cnpwstotbnd  38555  reheibor  38597  exidreslem  38635  divrngcl  38715  isdrngo2  38716  dibss  42050  xppss12  43107  arearect  44064  rtrclex  44465  rtrclexi  44469  rr2sscn2  46203  fourierdlem42  46985  opnvonmbllem2  47469  rngcrescrhmALTV  49203  imaidfu  50044  imasubc  50085