Theorem xpss12 5640

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3890  {copab 5141   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-opab 5142  df-xp 5631

This theorem is referenced by:  xpss  5641  inxpssres  5642  xpss1  5644  xpss2  5645  djussxp  5794  ssxpb  6132  resssxp  6228  cossxp  6230  relrelss  6231  fssxp  6689  oprabss  7471  oprres  7531  fimaproj  8082  xpord2pred  8092  xpord3pred  8099  naddcllem  8609  naddov2  8612  naddunif  8626  naddasslem1  8627  naddasslem2  8628  pmss12g  8814  marypha1lem  9343  marypha2lem1  9345  hartogslem1  9454  infxpenlem  9933  dfac5lem4  10046  dfac5lem4OLD  10048  axdc4lem  10375  fpwwe2lem1  10552  fpwwe2lem10  10561  fpwwe2lem11  10562  fpwwe2lem12  10563  canthwe  10572  tskxpss  10693  dmaddpi  10811  dmmulpi  10812  addnqf  10869  mulnqf  10870  rexpssxrxp  11188  ltrelxr  11204  mulnzcnf  11794  dfz2  12541  elq  12898  leiso  14419  znnen  16177  phimullem  16747  imasless  17502  sscpwex  17780  fullsubc  17815  fullresc  17816  wunfunc  17866  funcres2c  17868  homaf  17995  dmcoass  18031  catcoppccl  18082  catcfuccl  18083  catcxpccl  18171  rnghmresfn  20598  rnghmsscmap2  20608  rnghmsscmap  20609  rhmresfn  20627  rhmsscmap2  20637  rhmsscmap  20638  rhmsscrnghm  20644  rngcrescrhm  20663  znleval  21536  txuni2  23555  txbas  23557  txcld  23593  txcls  23594  neitx  23597  txcnp  23610  txlly  23626  txnlly  23627  hausdiag  23635  tx1stc  23640  txkgen  23642  xkococnlem  23649  cnmpt2res  23667  clssubg  24099  tsmsxplem1  24143  tsmsxplem2  24144  tsmsxp  24145  trust  24219  ustuqtop1  24231  psmetres2  24304  xmetres2  24351  metres2  24353  ressprdsds  24361  xmetresbl  24427  ressxms  24515  metustexhalf  24546  cfilucfil  24549  restmetu  24560  nrginvrcn  24682  qtopbaslem  24748  tgqioo  24790  re2ndc  24791  resubmet  24792  xrsdsre  24801  bndth  24950  lebnumii  24958  iscfil2  25258  cmssmscld  25342  cmsss  25343  cmscsscms  25365  minveclem3a  25419  ovolfsf  25463  opnmblALT  25595  mbfimaopnlem  25647  itg1addlem4  25691  limccnp2  25884  taylfval  26349  taylf  26351  mpodvdsmulf1o  27182  fsumdvdsmul  27183  dvdsmulf1o  27184  elzs  28401  sspg  30824  ssps  30826  sspmlem  30828  issh2  31305  hhssabloilem  31357  hhssabloi  31358  hhssnv  31360  hhshsslem1  31363  shsel  31410  iunxpssiun1  32664  ofrn2  32739  djussxp2  32747  gtiso  32800  xrofsup  32866  gsumwrd2dccatlem  33165  txomap  34025  tpr2rico  34103  prsss  34107  raddcn  34120  xrge0pluscn  34131  br2base  34460  dya2iocnrect  34472  dya2iocucvr  34475  eulerpartlemgh  34569  eulerpartlemgs2  34571  cvmlift2lem9  35546  cvmlift2lem10  35547  cvmlift2lem11  35548  cvmlift2lem12  35549  mpstssv  35774  elxp8  37740  mblfinlem2  38032  ftc1anc  38075  ssbnd  38162  prdsbnd2  38169  cnpwstotbnd  38171  reheibor  38213  exidreslem  38251  divrngcl  38331  isdrngo2  38332  dibss  41668  xppss12  42723  arearect  43667  rtrclex  44068  rtrclexi  44072  rr2sscn2  45817  fourierdlem42  46599  opnvonmbllem2  47083  rngcrescrhmALTV  48778  imaidfu  49607  imasubc  49648