Theorem xpss12 5665

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895  {copab 5166   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-opab 5167  df-xp 5656

This theorem is used by:  xpss  5666  inxpssres  5667  xpss1  5669  xpss2  5670  djussxp  5822  ssxpb  6165  resssxp  6272  cossxp  6274  relrelss  6275  fssxp  6737  oprabss  7528  oprres  7588  fimaproj  8154  xpord2pred  8164  xpord3pred  8171  naddcllem  8688  naddov2  8691  naddunif  8706  naddasslem1  8707  naddasslem2  8708  pmss12g  8900  marypha1lem  9428  marypha2lem1  9430  hartogslem1  9539  infxpenlem  10095  dfac5lem4  10208  axdc4lem  10536  fpwwe2lem1  10719  fpwwe2lem10  10728  fpwwe2lem11  10729  fpwwe2lem12  10730  canthwe  10739  tskxpss  10860  dmaddpi  10978  dmmulpi  10979  addnqf  11036  mulnqf  11037  rexpssxrxp  11357  ltrelxr  11373  mulnzcnf  11965  dfz2  12715  elq  13080  leiso  14607  znnen  16385  phimullem  16961  imasless  17717  sscpwex  17995  fullsubc  18030  fullresc  18031  wunfunc  18081  funcres2c  18083  homaf  18210  dmcoass  18246  catcoppccl  18297  catcfuccl  18298  catcxpccl  18386  rnghmresfn  20876  rnghmsscmap2  20886  rnghmsscmap  20887  rhmresfn  20905  rhmsscmap2  20915  rhmsscmap  20916  rhmsscrnghm  20922  rngcrescrhm  20941  znleval  21865  txuni2  23889  txbas  23891  txcld  23927  txcls  23928  neitx  23931  txcnp  23944  txlly  23960  txnlly  23961  hausdiag  23969  tx1stc  23974  txkgen  23976  xkococnlem  23983  cnmpt2res  24001  clssubg  24433  tsmsxplem1  24477  tsmsxplem2  24478  tsmsxp  24479  trust  24553  ustuqtop1  24565  psmetres2  24638  xmetres2  24685  metres2  24687  ressprdsds  24695  xmetresbl  24761  ressxms  24849  metustexhalf  24880  cfilucfil  24883  restmetu  24894  nrginvrcn  25016  qtopbaslem  25082  tgqioo  25124  re2ndc  25125  resubmet  25126  xrsdsre  25135  bndth  25284  lebnumii  25292  iscfil2  25592  cmssmscld  25676  cmsss  25677  cmscsscms  25699  minveclem3a  25753  ovolfsf  25797  opnmblALT  25929  mbfimaopnlem  25981  itg1addlem4  26025  limccnp2  26217  taylfval  26691  taylf  26693  mpodvdsmulf1o  27526  fsumdvdsmul  27527  dvdsmulf1o  27528  elzs  28775  sspg  31335  ssps  31337  sspmlem  31339  issh2  31816  hhssabloilem  31868  hhssabloi  31869  hhssnv  31871  hhshsslem1  31874  shsel  31921  iunxpssiun1  33209  ofrn2  33281  djussxp2  33289  gtiso  33341  xrofsup  33405  gsumwrd2dccatlem  33684  txomap  34512  tpr2rico  34590  prsss  34594  raddcn  34607  xrge0pluscn  34618  br2base  34947  dya2iocnrect  34959  dya2iocucvr  34962  eulerpartlemgh  35056  eulerpartlemgs2  35058  abweex  35769  cvmlift2lem9  36162  cvmlift2lem10  36163  cvmlift2lem11  36164  cvmlift2lem12  36165  mpstssv  36390  nmulprop  37031  elxp8  38387  mblfinlem2  38669  ftc1anc  38712  ssbnd  38815  prdsbnd2  38822  cnpwstotbnd  38824  reheibor  38866  exidreslem  38904  divrngcl  38984  isdrngo2  38985  dibss  42319  xppss12  43376  arearect  44310  rtrclex  44710  rtrclexi  44714  ishfstruct  46121  rr2sscn2  46470  fourierdlem42  47252  opnvonmbllem2  47736  rngcrescrhmALTV  49470  imaidfu  50319  imasubc  50360