ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpss12 GIF version

Theorem xpss12 4533
Description: Subset theorem for cross 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.
StepHypRef Expression
1 ssel 3017 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3017 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 565 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 4096 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 4434 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 4434 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 3065 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1438  wss 2997  {copab 3890   × cxp 4426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-in 3003  df-ss 3010  df-opab 3892  df-xp 4434
This theorem is referenced by:  xpss  4534  xpss1  4536  xpss2  4537  djussxp  4569  ssxpbm  4853  ssrnres  4860  cossxp  4940  cossxp2  4941  cocnvss  4943  relrelss  4944  fssxp  5163  oprabss  5716  pmss12g  6412  caserel  6757  casef  6758  dmaddpi  6863  dmmulpi  6864  rexpssxrxp  7511  ltrelxr  7526  dfz2  8789  eucialg  11123  phimullem  11283
  Copyright terms: Public domain W3C validator