Theorem xpss12 5543

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   ⊆ wss 3860  {copab 5098   × cxp 5526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-opab 5099  df-xp 5534

This theorem is referenced by:  xpss  5544  inxpssres  5545  xpss1  5547  xpss2  5548  djussxp  5691  ssxpb  6008  resssxp  6104  cossxp  6106  relrelss  6107  fssxp  6524  oprabss  7260  oprres  7318  fimaproj  7840  pmss12g  8464  marypha1lem  8943  marypha2lem1  8945  hartogslem1  9052  infxpenlem  9486  dfac5lem4  9599  axdc4lem  9928  fpwwe2lem1  10104  fpwwe2lem10  10113  fpwwe2lem11  10114  fpwwe2lem12  10115  canthwe  10124  tskxpss  10245  dmaddpi  10363  dmmulpi  10364  addnqf  10421  mulnqf  10422  rexpssxrxp  10737  ltrelxr  10753  mulnzcnopr  11337  dfz2  12052  elq  12403  leiso  13882  znnen  15626  phimullem  16184  imasless  16884  sscpwex  17157  fullsubc  17192  fullresc  17193  wunfunc  17241  funcres2c  17243  homaf  17369  dmcoass  17405  catcoppccl  17447  catcfuccl  17448  catcxpccl  17536  znleval  20335  txuni2  22278  txbas  22280  txcld  22316  txcls  22317  neitx  22320  txcnp  22333  txlly  22349  txnlly  22350  hausdiag  22358  tx1stc  22363  txkgen  22365  xkococnlem  22372  cnmpt2res  22390  clssubg  22822  tsmsxplem1  22866  tsmsxplem2  22867  tsmsxp  22868  trust  22943  ustuqtop1  22955  psmetres2  23029  xmetres2  23076  metres2  23078  ressprdsds  23086  xmetresbl  23152  ressxms  23240  metustexhalf  23271  cfilucfil  23274  restmetu  23285  nrginvrcn  23407  qtopbaslem  23473  tgqioo  23514  re2ndc  23515  resubmet  23516  xrsdsre  23524  bndth  23672  lebnumii  23680  iscfil2  23979  cmssmscld  24063  cmsss  24064  cmscsscms  24086  minveclem3a  24140  ovolfsf  24184  opnmblALT  24316  mbfimaopnlem  24368  itg1addlem4  24412  limccnp2  24604  taylfval  25066  taylf  25068  dvdsmulf1o  25891  fsumdvdsmul  25892  sspg  28623  ssps  28625  sspmlem  28627  issh2  29104  hhssabloilem  29156  hhssabloi  29157  hhssnv  29159  hhshsslem1  29162  shsel  29209  ofrn2  30512  djussxp2  30520  gtiso  30569  xrofsup  30626  txomap  31317  tpr2rico  31395  prsss  31399  raddcn  31412  xrge0pluscn  31423  br2base  31767  dya2iocnrect  31779  dya2iocucvr  31782  eulerpartlemgh  31876  eulerpartlemgs2  31878  cvmlift2lem9  32801  cvmlift2lem10  32802  cvmlift2lem11  32803  cvmlift2lem12  32804  mpstssv  33029  xpord2pred  33359  xpord3pred  33365  naddcllem  33428  naddov2  33431  addscllem1  33714  elxp8  35102  mblfinlem2  35409  ftc1anc  35452  ssbnd  35540  prdsbnd2  35547  cnpwstotbnd  35549  reheibor  35591  exidreslem  35629  divrngcl  35709  isdrngo2  35710  dibss  38779  xppss12  39746  arearect  40573  rtrclex  40725  rtrclexi  40729  rr2sscn2  42401  fourierdlem42  43192  opnvonmbllem2  43673  rnghmresfn  45003  rnghmsscmap2  45013  rnghmsscmap  45014  rhmresfn  45049  rhmsscmap2  45059  rhmsscmap  45060  rhmsscrnghm  45066  rngcrescrhm  45125  rngcrescrhmALTV  45143