Theorem xpss12 5691

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ⊆ wss 3948  {copab 5210   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682

This theorem is referenced by:  xpss  5692  inxpssres  5693  xpss1  5695  xpss2  5696  djussxp  5844  ssxpb  6171  resssxp  6267  cossxp  6269  relrelss  6270  fssxp  6743  oprabss  7512  oprres  7572  fimaproj  8118  xpord2pred  8128  xpord3pred  8135  naddcllem  8672  naddov2  8675  naddunif  8689  naddasslem1  8690  naddasslem2  8691  pmss12g  8860  marypha1lem  9425  marypha2lem1  9427  hartogslem1  9534  infxpenlem  10005  dfac5lem4  10118  axdc4lem  10447  fpwwe2lem1  10623  fpwwe2lem10  10632  fpwwe2lem11  10633  fpwwe2lem12  10634  canthwe  10643  tskxpss  10764  dmaddpi  10882  dmmulpi  10883  addnqf  10940  mulnqf  10941  rexpssxrxp  11256  ltrelxr  11272  mulnzcnopr  11857  dfz2  12574  elq  12931  leiso  14417  znnen  16152  phimullem  16709  imasless  17483  sscpwex  17759  fullsubc  17797  fullresc  17798  wunfunc  17846  wunfuncOLD  17847  funcres2c  17849  homaf  17977  dmcoass  18013  catcoppccl  18064  catcoppcclOLD  18065  catcfuccl  18066  catcfucclOLD  18067  catcxpccl  18156  catcxpcclOLD  18157  znleval  21102  txuni2  23061  txbas  23063  txcld  23099  txcls  23100  neitx  23103  txcnp  23116  txlly  23132  txnlly  23133  hausdiag  23141  tx1stc  23146  txkgen  23148  xkococnlem  23155  cnmpt2res  23173  clssubg  23605  tsmsxplem1  23649  tsmsxplem2  23650  tsmsxp  23651  trust  23726  ustuqtop1  23738  psmetres2  23812  xmetres2  23859  metres2  23861  ressprdsds  23869  xmetresbl  23935  ressxms  24026  metustexhalf  24057  cfilucfil  24060  restmetu  24071  nrginvrcn  24201  qtopbaslem  24267  tgqioo  24308  re2ndc  24309  resubmet  24310  xrsdsre  24318  bndth  24466  lebnumii  24474  iscfil2  24775  cmssmscld  24859  cmsss  24860  cmscsscms  24882  minveclem3a  24936  ovolfsf  24980  opnmblALT  25112  mbfimaopnlem  25164  itg1addlem4  25208  itg1addlem4OLD  25209  limccnp2  25401  taylfval  25863  taylf  25865  dvdsmulf1o  26688  fsumdvdsmul  26689  sspg  29969  ssps  29971  sspmlem  29973  issh2  30450  hhssabloilem  30502  hhssabloi  30503  hhssnv  30505  hhshsslem1  30508  shsel  30555  ofrn2  31853  djussxp2  31861  gtiso  31910  xrofsup  31968  txomap  32803  tpr2rico  32881  prsss  32885  raddcn  32898  xrge0pluscn  32909  br2base  33257  dya2iocnrect  33269  dya2iocucvr  33272  eulerpartlemgh  33366  eulerpartlemgs2  33368  cvmlift2lem9  34291  cvmlift2lem10  34292  cvmlift2lem11  34293  cvmlift2lem12  34294  mpstssv  34519  elxp8  36241  mblfinlem2  36515  ftc1anc  36558  ssbnd  36645  prdsbnd2  36652  cnpwstotbnd  36654  reheibor  36696  exidreslem  36734  divrngcl  36814  isdrngo2  36815  dibss  40029  xppss12  41044  arearect  41950  rtrclex  42354  rtrclexi  42358  rr2sscn2  44063  fourierdlem42  44852  opnvonmbllem2  45336  rnghmresfn  46815  rnghmsscmap2  46825  rnghmsscmap  46826  rhmresfn  46861  rhmsscmap2  46871  rhmsscmap  46872  rhmsscrnghm  46878  rngcrescrhm  46937  rngcrescrhmALTV  46955