Theorem xpss12 5678

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3906  {copab 5174   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3923  df-opab 5175  df-xp 5669

This theorem is referenced by:  xpss  5679  inxpssres  5680  xpss1  5682  xpss2  5683  djussxp  5833  ssxpb  6174  resssxp  6273  cossxp  6275  relrelss  6276  fssxp  6735  oprabss  7520  oprres  7580  fimaproj  8132  xpord2pred  8142  xpord3pred  8149  naddcllem  8663  naddov2  8666  naddunif  8681  naddasslem1  8682  naddasslem2  8683  pmss12g  8868  marypha1lem  9394  marypha2lem1  9396  hartogslem1  9505  infxpenlem  9998  dfac5lem4  10111  axdc4lem  10440  fpwwe2lem1  10617  fpwwe2lem10  10626  fpwwe2lem11  10627  fpwwe2lem12  10628  canthwe  10637  tskxpss  10758  dmaddpi  10876  dmmulpi  10877  addnqf  10934  mulnqf  10935  rexpssxrxp  11255  ltrelxr  11271  mulnzcnf  11861  dfz2  12611  elq  12975  leiso  14498  znnen  16269  phimullem  16839  imasless  17595  sscpwex  17873  fullsubc  17908  fullresc  17909  wunfunc  17959  funcres2c  17961  homaf  18088  dmcoass  18124  catcoppccl  18175  catcfuccl  18176  catcxpccl  18264  rnghmresfn  20705  rnghmsscmap2  20715  rnghmsscmap  20716  rhmresfn  20734  rhmsscmap2  20744  rhmsscmap  20745  rhmsscrnghm  20751  rngcrescrhm  20770  znleval  21685  txuni2  23703  txbas  23705  txcld  23741  txcls  23742  neitx  23745  txcnp  23758  txlly  23774  txnlly  23775  hausdiag  23783  tx1stc  23788  txkgen  23790  xkococnlem  23797  cnmpt2res  23815  clssubg  24247  tsmsxplem1  24291  tsmsxplem2  24292  tsmsxp  24293  trust  24367  ustuqtop1  24379  psmetres2  24452  xmetres2  24499  metres2  24501  ressprdsds  24509  xmetresbl  24575  ressxms  24663  metustexhalf  24694  cfilucfil  24697  restmetu  24708  nrginvrcn  24830  qtopbaslem  24896  tgqioo  24938  re2ndc  24939  resubmet  24940  xrsdsre  24949  bndth  25098  lebnumii  25106  iscfil2  25406  cmssmscld  25490  cmsss  25491  cmscsscms  25513  minveclem3a  25567  ovolfsf  25611  opnmblALT  25743  mbfimaopnlem  25795  itg1addlem4  25839  limccnp2  26032  taylfval  26500  taylf  26502  mpodvdsmulf1o  27336  fsumdvdsmul  27337  dvdsmulf1o  27338  elzs  28555  sspg  31058  ssps  31060  sspmlem  31062  issh2  31539  hhssabloilem  31591  hhssabloi  31592  hhssnv  31594  hhshsslem1  31597  shsel  31644  iunxpssiun1  32891  ofrn2  32963  djussxp2  32971  gtiso  33024  xrofsup  33090  gsumwrd2dccatlem  33375  txomap  34202  tpr2rico  34280  prsss  34284  raddcn  34297  xrge0pluscn  34308  br2base  34637  dya2iocnrect  34649  dya2iocucvr  34652  eulerpartlemgh  34746  eulerpartlemgs2  34748  cvmlift2lem9  35781  cvmlift2lem10  35782  cvmlift2lem11  35783  cvmlift2lem12  35784  mpstssv  36009  nmulprop  36660  elxp8  37995  mblfinlem2  38287  ftc1anc  38330  ssbnd  38417  prdsbnd2  38424  cnpwstotbnd  38426  reheibor  38468  exidreslem  38506  divrngcl  38586  isdrngo2  38587  dibss  41921  xppss12  42978  arearect  43922  rtrclex  44323  rtrclexi  44327  rr2sscn2  46061  fourierdlem42  46843  opnvonmbllem2  47327  rngcrescrhmALTV  49022  imaidfu  49865  imasubc  49906