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

Theorem xpss12 4655
 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 3097 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3097 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 588 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 4209 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 4554 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 4554 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 3146 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481   ⊆ wss 3077  {copab 3997   × cxp 4546 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-in 3083  df-ss 3090  df-opab 3999  df-xp 4554 This theorem is referenced by:  xpss  4656  xpss1  4658  xpss2  4659  djussxp  4693  ssxpbm  4983  ssrnres  4990  cossxp  5070  cossxp2  5071  cocnvss  5073  relrelss  5074  fssxp  5299  oprabss  5866  pmss12g  6578  caserel  6982  casef  6983  dmaddpi  7177  dmmulpi  7178  rexpssxrxp  7854  ltrelxr  7869  dfz2  9167  phimullem  11957  txuni2  12484  txbas  12486  neitx  12496  txcnp  12499  cnmpt2res  12525  psmetres2  12561  xmetres2  12607  metres2  12609  xmetresbl  12668  xmettx  12738  qtopbasss  12749  tgqioo  12775  resubmet  12776  limccnp2lem  12873  limccnp2cntop  12874
 Copyright terms: Public domain W3C validator