Theorem xpss12 5666

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ⊆ wss 3899  {copab 5167   × cxp 5649

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-opab 5168  df-xp 5657

This theorem is used by:  xpss  5667  inxpssres  5668  xpss1  5670  xpss2  5671  djussxp  5823  ssxpb  6165  resssxp  6265  cossxp  6267  relrelss  6268  fssxp  6729  oprabss  7520  oprres  7580  fimaproj  8136  xpord2pred  8146  xpord3pred  8153  naddcllem  8669  naddov2  8672  naddunif  8687  naddasslem1  8688  naddasslem2  8689  pmss12g  8881  marypha1lem  9409  marypha2lem1  9411  hartogslem1  9520  infxpenlem  10073  dfac5lem4  10186  axdc4lem  10514  fpwwe2lem1  10697  fpwwe2lem10  10706  fpwwe2lem11  10707  fpwwe2lem12  10708  canthwe  10717  tskxpss  10838  dmaddpi  10956  dmmulpi  10957  addnqf  11014  mulnqf  11015  rexpssxrxp  11335  ltrelxr  11351  mulnzcnf  11943  dfz2  12693  elq  13058  leiso  14584  znnen  16360  phimullem  16936  imasless  17692  sscpwex  17970  fullsubc  18005  fullresc  18006  wunfunc  18056  funcres2c  18058  homaf  18185  dmcoass  18221  catcoppccl  18272  catcfuccl  18273  catcxpccl  18361  rnghmresfn  20851  rnghmsscmap2  20861  rnghmsscmap  20862  rhmresfn  20880  rhmsscmap2  20890  rhmsscmap  20891  rhmsscrnghm  20897  rngcrescrhm  20916  znleval  21840  txuni2  23864  txbas  23866  txcld  23902  txcls  23903  neitx  23906  txcnp  23919  txlly  23935  txnlly  23936  hausdiag  23944  tx1stc  23949  txkgen  23951  xkococnlem  23958  cnmpt2res  23976  clssubg  24408  tsmsxplem1  24452  tsmsxplem2  24453  tsmsxp  24454  trust  24528  ustuqtop1  24540  psmetres2  24613  xmetres2  24660  metres2  24662  ressprdsds  24670  xmetresbl  24736  ressxms  24824  metustexhalf  24855  cfilucfil  24858  restmetu  24869  nrginvrcn  24991  qtopbaslem  25057  tgqioo  25099  re2ndc  25100  resubmet  25101  xrsdsre  25110  bndth  25259  lebnumii  25267  iscfil2  25567  cmssmscld  25651  cmsss  25652  cmscsscms  25674  minveclem3a  25728  ovolfsf  25772  opnmblALT  25904  mbfimaopnlem  25956  itg1addlem4  26000  limccnp2  26192  taylfval  26668  taylf  26670  mpodvdsmulf1o  27503  fsumdvdsmul  27504  dvdsmulf1o  27505  elzs  28752  sspg  31312  ssps  31314  sspmlem  31316  issh2  31793  hhssabloilem  31845  hhssabloi  31846  hhssnv  31848  hhshsslem1  31851  shsel  31898  iunxpssiun1  33144  ofrn2  33216  djussxp2  33224  gtiso  33276  xrofsup  33341  gsumwrd2dccatlem  33620  txomap  34448  tpr2rico  34526  prsss  34530  raddcn  34543  xrge0pluscn  34554  br2base  34884  dya2iocnrect  34896  dya2iocucvr  34899  eulerpartlemgh  34993  eulerpartlemgs2  34995  cvmlift2lem9  36045  cvmlift2lem10  36046  cvmlift2lem11  36047  cvmlift2lem12  36048  mpstssv  36273  nmulprop  36909  elxp8  38262  mblfinlem2  38544  ftc1anc  38587  ssbnd  38690  prdsbnd2  38697  cnpwstotbnd  38699  reheibor  38741  exidreslem  38779  divrngcl  38859  isdrngo2  38860  dibss  42194  xppss12  43251  arearect  44175  rtrclex  44576  rtrclexi  44580  rr2sscn2  46321  fourierdlem42  47103  opnvonmbllem2  47587  rngcrescrhmALTV  49321  imaidfu  50162  imasubc  50203