Theorem xpss12 5692

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ⊆ wss 3949  {copab 5211   × cxp 5675

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 3956  df-ss 3966  df-opab 5212  df-xp 5683

This theorem is referenced by:  xpss  5693  inxpssres  5694  xpss1  5696  xpss2  5697  djussxp  5846  ssxpb  6174  resssxp  6270  cossxp  6272  relrelss  6273  fssxp  6746  oprabss  7515  oprres  7575  fimaproj  8121  xpord2pred  8131  xpord3pred  8138  naddcllem  8675  naddov2  8678  naddunif  8692  naddasslem1  8693  naddasslem2  8694  pmss12g  8863  marypha1lem  9428  marypha2lem1  9430  hartogslem1  9537  infxpenlem  10008  dfac5lem4  10121  axdc4lem  10450  fpwwe2lem1  10626  fpwwe2lem10  10635  fpwwe2lem11  10636  fpwwe2lem12  10637  canthwe  10646  tskxpss  10767  dmaddpi  10885  dmmulpi  10886  addnqf  10943  mulnqf  10944  rexpssxrxp  11259  ltrelxr  11275  mulnzcnopr  11860  dfz2  12577  elq  12934  leiso  14420  znnen  16155  phimullem  16712  imasless  17486  sscpwex  17762  fullsubc  17800  fullresc  17801  wunfunc  17849  wunfuncOLD  17850  funcres2c  17852  homaf  17980  dmcoass  18016  catcoppccl  18067  catcoppcclOLD  18068  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  znleval  21110  txuni2  23069  txbas  23071  txcld  23107  txcls  23108  neitx  23111  txcnp  23124  txlly  23140  txnlly  23141  hausdiag  23149  tx1stc  23154  txkgen  23156  xkococnlem  23163  cnmpt2res  23181  clssubg  23613  tsmsxplem1  23657  tsmsxplem2  23658  tsmsxp  23659  trust  23734  ustuqtop1  23746  psmetres2  23820  xmetres2  23867  metres2  23869  ressprdsds  23877  xmetresbl  23943  ressxms  24034  metustexhalf  24065  cfilucfil  24068  restmetu  24079  nrginvrcn  24209  qtopbaslem  24275  tgqioo  24316  re2ndc  24317  resubmet  24318  xrsdsre  24326  bndth  24474  lebnumii  24482  iscfil2  24783  cmssmscld  24867  cmsss  24868  cmscsscms  24890  minveclem3a  24944  ovolfsf  24988  opnmblALT  25120  mbfimaopnlem  25172  itg1addlem4  25216  itg1addlem4OLD  25217  limccnp2  25409  taylfval  25871  taylf  25873  dvdsmulf1o  26698  fsumdvdsmul  26699  sspg  30012  ssps  30014  sspmlem  30016  issh2  30493  hhssabloilem  30545  hhssabloi  30546  hhssnv  30548  hhshsslem1  30551  shsel  30598  ofrn2  31896  djussxp2  31904  gtiso  31953  xrofsup  32011  txomap  32845  tpr2rico  32923  prsss  32927  raddcn  32940  xrge0pluscn  32951  br2base  33299  dya2iocnrect  33311  dya2iocucvr  33314  eulerpartlemgh  33408  eulerpartlemgs2  33410  cvmlift2lem9  34333  cvmlift2lem10  34334  cvmlift2lem11  34335  cvmlift2lem12  34336  mpstssv  34561  elxp8  36300  mblfinlem2  36574  ftc1anc  36617  ssbnd  36704  prdsbnd2  36711  cnpwstotbnd  36713  reheibor  36755  exidreslem  36793  divrngcl  36873  isdrngo2  36874  dibss  40088  xppss12  41095  arearect  42012  rtrclex  42416  rtrclexi  42420  rr2sscn2  44124  fourierdlem42  44913  opnvonmbllem2  45397  rnghmresfn  46909  rnghmsscmap2  46919  rnghmsscmap  46920  rhmresfn  46955  rhmsscmap2  46965  rhmsscmap  46966  rhmsscrnghm  46972  rngcrescrhm  47031  rngcrescrhmALTV  47049