Theorem xpss12 5670

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900  {copab 5170   × cxp 5653

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-opab 5171  df-xp 5661

This theorem is used by:  xpss  5671  inxpssres  5672  xpss1  5674  xpss2  5675  djussxp  5829  ssxpb  6178  resssxp  6290  cossxp  6292  relrelss  6293  fssxp  6759  oprabss  7551  oprres  7612  fimaproj  8179  xpord2pred  8189  xpord3pred  8196  naddcllem  8713  naddov2  8716  naddunif  8731  naddasslem1  8732  naddasslem2  8733  pmss12g  8925  marypha1lem  9452  marypha2lem1  9454  hartogslem1  9563  infxpenlem  10119  dfac5lem4  10232  axdc4lem  10560  fpwwe2lem1  10743  fpwwe2lem10  10752  fpwwe2lem11  10753  fpwwe2lem12  10754  canthwe  10763  tskxpss  10884  dmaddpi  11002  dmmulpi  11003  addnqf  11060  mulnqf  11061  rexpssxrxp  11381  ltrelxr  11397  mulnzcnf  11989  dfz2  12739  elq  13104  leiso  14631  znnen  16409  phimullem  16985  imasless  17741  sscpwex  18019  fullsubc  18054  fullresc  18055  wunfunc  18105  funcres2c  18107  homaf  18234  dmcoass  18270  catcoppccl  18321  catcfuccl  18322  catcxpccl  18410  rnghmresfn  20901  rnghmsscmap2  20911  rnghmsscmap  20912  rhmresfn  20930  rhmsscmap2  20940  rhmsscmap  20941  rhmsscrnghm  20947  rngcrescrhm  20966  znleval  21890  txuni2  23914  txbas  23916  txcld  23952  txcls  23953  neitx  23956  txcnp  23969  txlly  23985  txnlly  23986  hausdiag  23994  tx1stc  23999  txkgen  24001  xkococnlem  24008  cnmpt2res  24026  clssubg  24458  tsmsxplem1  24502  tsmsxplem2  24503  tsmsxp  24504  trust  24578  ustuqtop1  24590  psmetres2  24663  xmetres2  24710  metres2  24712  ressprdsds  24720  xmetresbl  24786  ressxms  24874  metustexhalf  24905  cfilucfil  24908  restmetu  24919  nrginvrcn  25041  qtopbaslem  25107  tgqioo  25149  re2ndc  25150  resubmet  25151  xrsdsre  25160  bndth  25309  lebnumii  25317  iscfil2  25617  cmssmscld  25701  cmsss  25702  cmscsscms  25724  minveclem3a  25778  ovolfsf  25822  opnmblALT  25954  mbfimaopnlem  26006  itg1addlem4  26050  limccnp2  26242  taylfval  26716  taylf  26718  mpodvdsmulf1o  27551  fsumdvdsmul  27552  dvdsmulf1o  27553  elzs  28800  sspg  31360  ssps  31362  sspmlem  31364  issh2  31841  hhssabloilem  31893  hhssabloi  31894  hhssnv  31896  hhshsslem1  31899  shsel  31946  iunxpssiun1  33234  ofrn2  33306  djussxp2  33314  gtiso  33365  xrofsup  33429  gsumwrd2dccatlem  33708  txomap  34536  tpr2rico  34614  prsss  34618  raddcn  34631  xrge0pluscn  34642  br2base  34971  dya2iocnrect  34983  dya2iocucvr  34986  eulerpartlemgh  35080  eulerpartlemgs2  35082  abweex  35801  cvmlift2lem9  36243  cvmlift2lem10  36244  cvmlift2lem11  36245  cvmlift2lem12  36246  mpstssv  36471  nmulprop  37117  elxp8  38486  mblfinlem2  38768  ftc1anc  38811  ssbnd  38914  prdsbnd2  38921  cnpwstotbnd  38923  reheibor  38965  exidreslem  39003  divrngcl  39083  isdrngo2  39084  dibss  42418  xppss12  43476  arearect  44409  rtrclex  44809  rtrclexi  44813  ishfstruct  46226  rr2sscn2  46582  fourierdlem42  47364  opnvonmbllem2  47848  rngcrescrhmALTV  49582  imaidfu  50431  imasubc  50472