Theorem xpss12 5573

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113   ⊆ wss 3939  {copab 5131   × cxp 5556

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-in 3946  df-ss 3955  df-opab 5132  df-xp 5564

This theorem is referenced by:  xpss  5574  inxpssres  5575  xpss1  5577  xpss2  5578  djussxp  5719  ssxpb  6034  cossxp  6126  relrelss  6127  fssxp  6537  oprabss  7263  oprres  7319  fimaproj  7832  pmss12g  8436  marypha1lem  8900  marypha2lem1  8902  hartogslem1  9009  infxpenlem  9442  dfac5lem4  9555  axdc4lem  9880  fpwwe2lem1  10056  fpwwe2lem11  10065  fpwwe2lem12  10066  fpwwe2lem13  10067  canthwe  10076  tskxpss  10197  dmaddpi  10315  dmmulpi  10316  addnqf  10373  mulnqf  10374  rexpssxrxp  10689  ltrelxr  10705  mulnzcnopr  11289  dfz2  12003  elq  12353  leiso  13820  znnen  15568  phimullem  16119  imasless  16816  sscpwex  17088  fullsubc  17123  fullresc  17124  wunfunc  17172  funcres2c  17174  homaf  17293  dmcoass  17329  catcoppccl  17371  catcfuccl  17372  catcxpccl  17460  znleval  20704  txuni2  22176  txbas  22178  txcld  22214  txcls  22215  neitx  22218  txcnp  22231  txlly  22247  txnlly  22248  hausdiag  22256  tx1stc  22261  txkgen  22263  xkococnlem  22270  cnmpt2res  22288  clssubg  22720  tsmsxplem1  22764  tsmsxplem2  22765  tsmsxp  22766  trust  22841  ustuqtop1  22853  psmetres2  22927  xmetres2  22974  metres2  22976  ressprdsds  22984  xmetresbl  23050  ressxms  23138  metustexhalf  23169  cfilucfil  23172  restmetu  23183  nrginvrcn  23304  qtopbaslem  23370  tgqioo  23411  re2ndc  23412  resubmet  23413  xrsdsre  23421  bndth  23565  lebnumii  23573  iscfil2  23872  cmssmscld  23956  cmsss  23957  cmscsscms  23979  minveclem3a  24033  ovolfsf  24075  opnmblALT  24207  mbfimaopnlem  24259  itg1addlem4  24303  limccnp2  24493  taylfval  24950  taylf  24952  dvdsmulf1o  25774  fsumdvdsmul  25775  sspg  28508  ssps  28510  sspmlem  28512  issh2  28989  hhssabloilem  29041  hhssabloi  29042  hhssnv  29044  hhshsslem1  29047  shsel  29094  ofrn2  30390  gtiso  30439  xrofsup  30495  txomap  31102  tpr2rico  31159  prsss  31163  raddcn  31176  xrge0pluscn  31187  br2base  31531  dya2iocnrect  31543  dya2iocucvr  31546  eulerpartlemgh  31640  eulerpartlemgs2  31642  cvmlift2lem9  32562  cvmlift2lem10  32563  cvmlift2lem11  32564  cvmlift2lem12  32565  mpstssv  32790  elxp8  34656  mblfinlem2  34934  ftc1anc  34979  ssbnd  35070  prdsbnd2  35077  cnpwstotbnd  35079  reheibor  35121  exidreslem  35159  divrngcl  35239  isdrngo2  35240  dibss  38309  xppss12  39121  arearect  39828  rtrclex  39983  rtrclexi  39987  rp-imass  40123  rr2sscn2  41640  fourierdlem42  42441  opnvonmbllem2  42922  rnghmresfn  44241  rnghmsscmap2  44251  rnghmsscmap  44252  rhmresfn  44287  rhmsscmap2  44297  rhmsscmap  44298  rhmsscrnghm  44304  rngcrescrhm  44363  rngcrescrhmALTV  44381