Theorem xpss12 5715

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3976  {copab 5228   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpss  5716  inxpssres  5717  xpss1  5719  xpss2  5720  djussxp  5870  ssxpb  6205  resssxp  6301  cossxp  6303  relrelss  6304  fssxp  6775  oprabss  7557  oprres  7618  fimaproj  8176  xpord2pred  8186  xpord3pred  8193  naddcllem  8732  naddov2  8735  naddunif  8749  naddasslem1  8750  naddasslem2  8751  pmss12g  8927  marypha1lem  9502  marypha2lem1  9504  hartogslem1  9611  infxpenlem  10082  dfac5lem4  10195  dfac5lem4OLD  10197  axdc4lem  10524  fpwwe2lem1  10700  fpwwe2lem10  10709  fpwwe2lem11  10710  fpwwe2lem12  10711  canthwe  10720  tskxpss  10841  dmaddpi  10959  dmmulpi  10960  addnqf  11017  mulnqf  11018  rexpssxrxp  11335  ltrelxr  11351  mulnzcnf  11936  dfz2  12658  elq  13015  leiso  14508  znnen  16260  phimullem  16826  imasless  17600  sscpwex  17876  fullsubc  17914  fullresc  17915  wunfunc  17965  wunfuncOLD  17966  funcres2c  17968  homaf  18097  dmcoass  18133  catcoppccl  18184  catcoppcclOLD  18185  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  rnghmresfn  20641  rnghmsscmap2  20651  rnghmsscmap  20652  rhmresfn  20670  rhmsscmap2  20680  rhmsscmap  20681  rhmsscrnghm  20687  rngcrescrhm  20706  znleval  21596  txuni2  23594  txbas  23596  txcld  23632  txcls  23633  neitx  23636  txcnp  23649  txlly  23665  txnlly  23666  hausdiag  23674  tx1stc  23679  txkgen  23681  xkococnlem  23688  cnmpt2res  23706  clssubg  24138  tsmsxplem1  24182  tsmsxplem2  24183  tsmsxp  24184  trust  24259  ustuqtop1  24271  psmetres2  24345  xmetres2  24392  metres2  24394  ressprdsds  24402  xmetresbl  24468  ressxms  24559  metustexhalf  24590  cfilucfil  24593  restmetu  24604  nrginvrcn  24734  qtopbaslem  24800  tgqioo  24841  re2ndc  24842  resubmet  24843  xrsdsre  24851  bndth  25009  lebnumii  25017  iscfil2  25319  cmssmscld  25403  cmsss  25404  cmscsscms  25426  minveclem3a  25480  ovolfsf  25525  opnmblALT  25657  mbfimaopnlem  25709  itg1addlem4  25753  itg1addlem4OLD  25754  limccnp2  25947  taylfval  26418  taylf  26420  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dvdsmulf1o  27257  fsumdvdsmulOLD  27258  elzs  28388  sspg  30760  ssps  30762  sspmlem  30764  issh2  31241  hhssabloilem  31293  hhssabloi  31294  hhssnv  31296  hhshsslem1  31299  shsel  31346  ofrn2  32659  djussxp2  32666  gtiso  32712  xrofsup  32774  txomap  33780  tpr2rico  33858  prsss  33862  raddcn  33875  xrge0pluscn  33886  br2base  34234  dya2iocnrect  34246  dya2iocucvr  34249  eulerpartlemgh  34343  eulerpartlemgs2  34345  cvmlift2lem9  35279  cvmlift2lem10  35280  cvmlift2lem11  35281  cvmlift2lem12  35282  mpstssv  35507  elxp8  37337  mblfinlem2  37618  ftc1anc  37661  ssbnd  37748  prdsbnd2  37755  cnpwstotbnd  37757  reheibor  37799  exidreslem  37837  divrngcl  37917  isdrngo2  37918  dibss  41126  xppss12  42222  arearect  43176  rtrclex  43579  rtrclexi  43583  rr2sscn2  45281  fourierdlem42  46070  opnvonmbllem2  46554  rngcrescrhmALTV  48003