Theorem xpss12 5327

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

Syntax hints:   → wi 4   ∧ wa 385   ∈ wcel 2157   ⊆ wss 3769  {copab 4905   × cxp 5310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-in 3776  df-ss 3783  df-opab 4906  df-xp 5318

This theorem is referenced by:  xpss  5328  inxpssres  5329  xpss1  5331  xpss2  5332  djussxp  5471  ssxpb  5785  cossxp  5877  relrelss  5878  fssxp  6275  oprabss  6980  oprres  7036  pmss12g  8122  marypha1lem  8581  marypha2lem1  8583  hartogslem1  8689  infxpenlem  9122  dfac5lem4  9235  axdc4lem  9565  fpwwe2lem1  9741  fpwwe2lem11  9750  fpwwe2lem12  9751  fpwwe2lem13  9752  canthwe  9761  tskxpss  9882  dmaddpi  10000  dmmulpi  10001  addnqf  10058  mulnqf  10059  rexpssxrxp  10373  ltrelxr  10389  mulnzcnopr  10965  dfz2  11684  elq  12035  leiso  13492  znnen  15277  phimullem  15817  imasless  16515  sscpwex  16789  fullsubc  16824  fullresc  16825  wunfunc  16873  funcres2c  16875  homaf  16994  dmcoass  17030  catcoppccl  17072  catcfuccl  17073  catcxpccl  17162  znleval  20224  txuni2  21697  txbas  21699  txcld  21735  txcls  21736  neitx  21739  txcnp  21752  txlly  21768  txnlly  21769  hausdiag  21777  tx1stc  21782  txkgen  21784  xkococnlem  21791  cnmpt2res  21809  clssubg  22240  tsmsxplem1  22284  tsmsxplem2  22285  tsmsxp  22286  trust  22361  ustuqtop1  22373  psmetres2  22447  xmetres2  22494  metres2  22496  ressprdsds  22504  xmetresbl  22570  ressxms  22658  metustexhalf  22689  cfilucfil  22692  restmetu  22703  nrginvrcn  22824  qtopbaslem  22890  tgqioo  22931  re2ndc  22932  resubmet  22933  xrsdsre  22941  bndth  23085  lebnumii  23093  iscfil2  23392  cmssmscld  23476  cmsss  23477  cmscsscms  23499  minveclem3a  23537  ovolfsf  23579  opnmblALT  23711  mbfimaopnlem  23763  itg1addlem4  23807  limccnp2  23997  taylfval  24454  taylf  24456  dvdsmulf1o  25272  fsumdvdsmul  25273  sspg  28108  ssps  28110  sspmlem  28112  issh2  28591  hhssabloilem  28643  hhssabloi  28644  hhssnv  28646  hhshsslem1  28649  shsel  28698  ofrn2  29961  gtiso  29996  xrofsup  30051  fimaproj  30416  txomap  30417  tpr2rico  30474  prsss  30478  raddcn  30491  xrge0pluscn  30502  br2base  30847  dya2iocnrect  30859  dya2iocucvr  30862  eulerpartlemgh  30956  eulerpartlemgs2  30958  cvmlift2lem9  31810  cvmlift2lem10  31811  cvmlift2lem11  31812  cvmlift2lem12  31813  mpstssv  31953  elxp8  33717  mblfinlem2  33936  ftc1anc  33981  ssbnd  34074  prdsbnd2  34081  cnpwstotbnd  34083  reheibor  34125  exidreslem  34163  divrngcl  34243  isdrngo2  34244  dibss  37190  xppss12  38037  arearect  38585  rtrclex  38707  rtrclexi  38711  rp-imass  38847  idhe  38863  rr2sscn2  40326  fourierdlem42  41109  opnvonmbllem2  41593  rnghmresfn  42762  rnghmsscmap2  42772  rnghmsscmap  42773  rhmresfn  42808  rhmsscmap2  42818  rhmsscmap  42819  rhmsscrnghm  42825  rngcrescrhm  42884  rngcrescrhmALTV  42902