Theorem xpss12 5681

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3908  {copab 5178   × cxp 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ss 3925  df-opab 5179  df-xp 5672

This theorem is used by:  xpss  5682  inxpssres  5683  xpss1  5685  xpss2  5686  djussxp  5836  ssxpb  6177  resssxp  6277  cossxp  6279  relrelss  6280  fssxp  6740  oprabss  7531  oprres  7591  fimaproj  8140  xpord2pred  8150  xpord3pred  8157  naddcllem  8671  naddov2  8674  naddunif  8689  naddasslem1  8690  naddasslem2  8691  pmss12g  8876  marypha1lem  9403  marypha2lem1  9405  hartogslem1  9514  infxpenlem  10016  dfac5lem4  10129  axdc4lem  10457  fpwwe2lem1  10634  fpwwe2lem10  10643  fpwwe2lem11  10644  fpwwe2lem12  10645  canthwe  10654  tskxpss  10775  dmaddpi  10893  dmmulpi  10894  addnqf  10951  mulnqf  10952  rexpssxrxp  11272  ltrelxr  11288  mulnzcnf  11878  dfz2  12628  elq  12992  leiso  14516  znnen  16293  phimullem  16863  imasless  17619  sscpwex  17897  fullsubc  17932  fullresc  17933  wunfunc  17983  funcres2c  17985  homaf  18112  dmcoass  18148  catcoppccl  18199  catcfuccl  18200  catcxpccl  18288  rnghmresfn  20755  rnghmsscmap2  20765  rnghmsscmap  20766  rhmresfn  20784  rhmsscmap2  20794  rhmsscmap  20795  rhmsscrnghm  20801  rngcrescrhm  20820  znleval  21741  txuni2  23759  txbas  23761  txcld  23797  txcls  23798  neitx  23801  txcnp  23814  txlly  23830  txnlly  23831  hausdiag  23839  tx1stc  23844  txkgen  23846  xkococnlem  23853  cnmpt2res  23871  clssubg  24303  tsmsxplem1  24347  tsmsxplem2  24348  tsmsxp  24349  trust  24423  ustuqtop1  24435  psmetres2  24508  xmetres2  24555  metres2  24557  ressprdsds  24565  xmetresbl  24631  ressxms  24719  metustexhalf  24750  cfilucfil  24753  restmetu  24764  nrginvrcn  24886  qtopbaslem  24952  tgqioo  24994  re2ndc  24995  resubmet  24996  xrsdsre  25005  bndth  25154  lebnumii  25162  iscfil2  25462  cmssmscld  25546  cmsss  25547  cmscsscms  25569  minveclem3a  25623  ovolfsf  25667  opnmblALT  25799  mbfimaopnlem  25851  itg1addlem4  25895  limccnp2  26088  taylfval  26559  taylf  26561  mpodvdsmulf1o  27395  fsumdvdsmul  27396  dvdsmulf1o  27397  elzs  28614  sspg  31117  ssps  31119  sspmlem  31121  issh2  31598  hhssabloilem  31650  hhssabloi  31651  hhssnv  31653  hhshsslem1  31656  shsel  31703  iunxpssiun1  32950  ofrn2  33022  djussxp2  33030  gtiso  33083  xrofsup  33149  gsumwrd2dccatlem  33428  txomap  34255  tpr2rico  34333  prsss  34337  raddcn  34350  xrge0pluscn  34361  br2base  34690  dya2iocnrect  34702  dya2iocucvr  34705  eulerpartlemgh  34799  eulerpartlemgs2  34801  cvmlift2lem9  35823  cvmlift2lem10  35824  cvmlift2lem11  35825  cvmlift2lem12  35826  mpstssv  36051  nmulprop  36702  elxp8  38057  mblfinlem2  38349  ftc1anc  38392  ssbnd  38479  prdsbnd2  38486  cnpwstotbnd  38488  reheibor  38530  exidreslem  38568  divrngcl  38648  isdrngo2  38649  dibss  41983  xppss12  43040  arearect  43982  rtrclex  44383  rtrclexi  44387  rr2sscn2  46121  fourierdlem42  46903  opnvonmbllem2  47387  rngcrescrhmALTV  49085  imaidfu  49928  imasubc  49969