Theorem xpss12 5703

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   ⊆ wss 3962  {copab 5209   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-opab 5210  df-xp 5694

This theorem is referenced by:  xpss  5704  inxpssres  5705  xpss1  5707  xpss2  5708  djussxp  5858  ssxpb  6195  resssxp  6291  cossxp  6293  relrelss  6294  fssxp  6763  oprabss  7539  oprres  7600  fimaproj  8158  xpord2pred  8168  xpord3pred  8175  naddcllem  8712  naddov2  8715  naddunif  8729  naddasslem1  8730  naddasslem2  8731  pmss12g  8907  marypha1lem  9470  marypha2lem1  9472  hartogslem1  9579  infxpenlem  10050  dfac5lem4  10163  dfac5lem4OLD  10165  axdc4lem  10492  fpwwe2lem1  10668  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe2lem12  10679  canthwe  10688  tskxpss  10809  dmaddpi  10927  dmmulpi  10928  addnqf  10985  mulnqf  10986  rexpssxrxp  11303  ltrelxr  11319  mulnzcnf  11906  dfz2  12629  elq  12989  leiso  14494  znnen  16244  phimullem  16812  imasless  17586  sscpwex  17862  fullsubc  17900  fullresc  17901  wunfunc  17951  wunfuncOLD  17952  funcres2c  17954  homaf  18083  dmcoass  18119  catcoppccl  18170  catcoppcclOLD  18171  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  rnghmresfn  20635  rnghmsscmap2  20645  rnghmsscmap  20646  rhmresfn  20664  rhmsscmap2  20674  rhmsscmap  20675  rhmsscrnghm  20681  rngcrescrhm  20700  znleval  21590  txuni2  23588  txbas  23590  txcld  23626  txcls  23627  neitx  23630  txcnp  23643  txlly  23659  txnlly  23660  hausdiag  23668  tx1stc  23673  txkgen  23675  xkococnlem  23682  cnmpt2res  23700  clssubg  24132  tsmsxplem1  24176  tsmsxplem2  24177  tsmsxp  24178  trust  24253  ustuqtop1  24265  psmetres2  24339  xmetres2  24386  metres2  24388  ressprdsds  24396  xmetresbl  24462  ressxms  24553  metustexhalf  24584  cfilucfil  24587  restmetu  24598  nrginvrcn  24728  qtopbaslem  24794  tgqioo  24835  re2ndc  24836  resubmet  24837  xrsdsre  24845  bndth  25003  lebnumii  25011  iscfil2  25313  cmssmscld  25397  cmsss  25398  cmscsscms  25420  minveclem3a  25474  ovolfsf  25519  opnmblALT  25651  mbfimaopnlem  25703  itg1addlem4  25747  itg1addlem4OLD  25748  limccnp2  25941  taylfval  26414  taylf  26416  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  elzs  28384  sspg  30756  ssps  30758  sspmlem  30760  issh2  31237  hhssabloilem  31289  hhssabloi  31290  hhssnv  31292  hhshsslem1  31295  shsel  31342  ofrn2  32656  djussxp2  32664  gtiso  32715  xrofsup  32777  gsumwrd2dccatlem  33051  txomap  33794  tpr2rico  33872  prsss  33876  raddcn  33889  xrge0pluscn  33900  br2base  34250  dya2iocnrect  34262  dya2iocucvr  34265  eulerpartlemgh  34359  eulerpartlemgs2  34361  cvmlift2lem9  35295  cvmlift2lem10  35296  cvmlift2lem11  35297  cvmlift2lem12  35298  mpstssv  35523  elxp8  37353  mblfinlem2  37644  ftc1anc  37687  ssbnd  37774  prdsbnd2  37781  cnpwstotbnd  37783  reheibor  37825  exidreslem  37863  divrngcl  37943  isdrngo2  37944  dibss  41151  xppss12  42246  arearect  43203  rtrclex  43606  rtrclexi  43610  rr2sscn2  45315  fourierdlem42  46104  opnvonmbllem2  46588  rngcrescrhmALTV  48123