Theorem ssel 2066

Description: Membership relationships follow from a subclass relationship.

Assertion

Ref	Expression
ssel	⊢ (A ⊆ B → (C ∈ A → C ∈ B))

Proof of Theorem ssel

Step	Hyp	Ref	Expression
1		dfss2 2061	. . . . . 6 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
2	1	biimp 151	. . . . 5 ⊢ (A ⊆ B → ∀x(x ∈ A → x ∈ B))
3	2	19.21bi 1062	. . . 4 ⊢ (A ⊆ B → (x ∈ A → x ∈ B))
4	3	anim2d 563	. . 3 ⊢ (A ⊆ B → ((x = C ⋀ x ∈ A) → (x = C ⋀ x ∈ B)))
5	4	19.22dv 1292	. 2 ⊢ (A ⊆ B → (∃x(x = C ⋀ x ∈ A) → ∃x(x = C ⋀ x ∈ B)))
6		df-clel 1475	. 2 ⊢ (C ∈ A ↔ ∃x(x = C ⋀ x ∈ A))
7		df-clel 1475	. 2 ⊢ (C ∈ B ↔ ∃x(x = C ⋀ x ∈ B))
8	5, 6, 7	3imtr4g 555	1 ⊢ (A ⊆ B → (C ∈ A → C ∈ B))

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 956   = wceq 958   ∈ wcel 960  ∃wex 982   ⊆ wss 2050

This theorem is referenced by:  ssel2 2067  sseli 2068  sseld 2070  ssralv 2117  ssrexv 2118  ssconb 2173  sscon 2174  ssdif 2175  reuss2 2278  reupick 2282  reldisj 2317  prss 2475  sssn 2477  tpss 2480  uniss 2525  iunss1 2578  ss2iun 2581  ssiun 2596  sspwb 2761  unipw 2762  pwssun 2833  poss 2847  soss 2858  reuuniss 2895  mouniss 2896  reuuniss2 2897  elpwunsn 2918  onfr 2992  ssorduni 2999  onint 3012  oninton 3018  oneqmini 3023  sucssel 3076  onssneli 3107  onssneli2 3108  snsn0non 3131  ssnlim 3173  brrelex 3213  weinxp 3239  ssrel 3253  ssxp 3262  cnvss 3297  dmss 3316  elreldm 3344  relssres 3398  iss 3403  resopab2 3404  cotr 3442  cnvsym 3443  ssrnres 3487  cores 3505  funss 3540  funopg 3553  funssres 3558  fununi 3569  dfimafn 3767  funimass4 3769  fvelimab 3771  funimass3 3812  dff2 3823  dff3 3824  rnssopab 3831  fopabcos 3839  funfvima2 3859  funfvima3 3860  isomin 3905  isofrlem 3907  tfrlem1 3917  tfrlem13 3929  tz7.48lem 3961  tz7.49 3965  omsmolem 4262  omsmo 4263  ss2ixp 4360  onomeneq 4525  unblem1 4551  unblem3 4553  fiint 4572  fiintOLD 4573  inf3lem2 4623  r1tr 4664  tz9.13 4673  rankr1lem 4683  rankel 4690  rankval3 4691  bndrank 4692  rankpw 4694  cardlim 4862  carduni 4869  cfub 4920  suplem1pr 5173  supsr 5243  suprelem 5271  pre-axsup 5303  lbreu 6047  lbinfm 6050  sup2 6053  sup3 6054  infm3 6056  infmsup 6070  infmrcl 6071  xrsupsslem 6078  xrinfmsslem 6079  supxrre 6085  supxrpnf 6090  supxrunb1 6091  supxrunb2 6092  uzwo4OLD 6212  uzwo5OLD 6213  iccsupr 6399  uzwo 6456  uzwoOLD 6457  infxpidmlem7 7559  infmap2lem1 7581  tgval3t 7624  basgen2t 7638  ntrss2 7687  elcls2 7702  cncnplem3 7773  metreslem 7819  opnin 7866  cncfmet 7902  metelcls 7962  ubthlem10 8534  ocsh 9151  occont 9155  ococss 9161  shorth 9163  shless 9342  spansnss2t 9493  h1datom 9499  pjss2 9620  pjssm 9621  pjorthco 10092  pj3s 10130  cnrsfin 10495  cmpmorp 10683

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain