Theorem xpss12 5534

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   ⊆ wss 3881  {copab 5092   × cxp 5517

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 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-opab 5093  df-xp 5525

This theorem is referenced by:  xpss  5535  inxpssres  5536  xpss1  5538  xpss2  5539  djussxp  5680  ssxpb  5998  resssxp  6089  cossxp  6091  relrelss  6092  fssxp  6508  oprabss  7239  oprres  7296  fimaproj  7812  pmss12g  8416  marypha1lem  8881  marypha2lem1  8883  hartogslem1  8990  infxpenlem  9424  dfac5lem4  9537  axdc4lem  9866  fpwwe2lem1  10042  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe2lem13  10053  canthwe  10062  tskxpss  10183  dmaddpi  10301  dmmulpi  10302  addnqf  10359  mulnqf  10360  rexpssxrxp  10675  ltrelxr  10691  mulnzcnopr  11275  dfz2  11988  elq  12338  leiso  13813  znnen  15557  phimullem  16106  imasless  16805  sscpwex  17077  fullsubc  17112  fullresc  17113  wunfunc  17161  funcres2c  17163  homaf  17282  dmcoass  17318  catcoppccl  17360  catcfuccl  17361  catcxpccl  17449  znleval  20246  txuni2  22170  txbas  22172  txcld  22208  txcls  22209  neitx  22212  txcnp  22225  txlly  22241  txnlly  22242  hausdiag  22250  tx1stc  22255  txkgen  22257  xkococnlem  22264  cnmpt2res  22282  clssubg  22714  tsmsxplem1  22758  tsmsxplem2  22759  tsmsxp  22760  trust  22835  ustuqtop1  22847  psmetres2  22921  xmetres2  22968  metres2  22970  ressprdsds  22978  xmetresbl  23044  ressxms  23132  metustexhalf  23163  cfilucfil  23166  restmetu  23177  nrginvrcn  23298  qtopbaslem  23364  tgqioo  23405  re2ndc  23406  resubmet  23407  xrsdsre  23415  bndth  23563  lebnumii  23571  iscfil2  23870  cmssmscld  23954  cmsss  23955  cmscsscms  23977  minveclem3a  24031  ovolfsf  24075  opnmblALT  24207  mbfimaopnlem  24259  itg1addlem4  24303  limccnp2  24495  taylfval  24954  taylf  24956  dvdsmulf1o  25779  fsumdvdsmul  25780  sspg  28511  ssps  28513  sspmlem  28515  issh2  28992  hhssabloilem  29044  hhssabloi  29045  hhssnv  29047  hhshsslem1  29050  shsel  29097  ofrn2  30401  djussxp2  30410  gtiso  30460  xrofsup  30518  txomap  31187  tpr2rico  31265  prsss  31269  raddcn  31282  xrge0pluscn  31293  br2base  31637  dya2iocnrect  31649  dya2iocucvr  31652  eulerpartlemgh  31746  eulerpartlemgs2  31748  cvmlift2lem9  32671  cvmlift2lem10  32672  cvmlift2lem11  32673  cvmlift2lem12  32674  mpstssv  32899  elxp8  34788  mblfinlem2  35095  ftc1anc  35138  ssbnd  35226  prdsbnd2  35233  cnpwstotbnd  35235  reheibor  35277  exidreslem  35315  divrngcl  35395  isdrngo2  35396  dibss  38465  xppss12  39409  arearect  40165  rtrclex  40317  rtrclexi  40321  rr2sscn2  41998  fourierdlem42  42791  opnvonmbllem2  43272  rnghmresfn  44587  rnghmsscmap2  44597  rnghmsscmap  44598  rhmresfn  44633  rhmsscmap2  44643  rhmsscmap  44644  rhmsscrnghm  44650  rngcrescrhm  44709  rngcrescrhmALTV  44727