Theorem sseld 2057

Description: Membership deduction from subclass relationship.

Hypothesis

Ref	Expression
sseld.1	⊢ (φ → A ⊆ B)

Assertion

Ref	Expression
sseld	⊢ (φ → (C ∈ A → C ∈ B))

Proof of Theorem sseld

Step	Hyp	Ref	Expression
1		sseld.1	. 2 ⊢ (φ → A ⊆ B)
2		ssel 2053	. 2 ⊢ (A ⊆ B → (C ∈ A → C ∈ B))
3	1, 2	syl 10	1 ⊢ (φ → (C ∈ A → C ∈ B))

Syntax hints:   → wi 3   ∈ wcel 955   ⊆ wss 2037

This theorem is referenced by:  sseldd 2058  ssbrd 2646  uniopel 2798  elrel 3243  dmrnssfld 3343  nfunv 3532  opelf 3625  fvimacnv 3790  ffvelrn 3799  1stdm 4093  oa00 4177  omordi 4181  omlimcl 4193  mapsn 4329  ixpf 4340  uniixp 4341  pssnn 4513  sucprcreg 4572  inf3lem2 4586  trcl 4617  r1ord 4627  rankwflem 4637  rankr1 4646  ssrankr1 4648  rankel 4652  r1pwcl 4659  rankuni2 4662  rankval4 4674  cplem1 4692  kmlem2 4738  zorn2lem7 4766  carduniima 4862  alephfp 4872  elprpq 5067  genpss 5079  ltexprlem7 5120  suprub 6003  uzind 6153  elfzp1 6442  fsequb 6455  fsequb2 6456  seqzfveq 6486  fsump1s 6951  fsumcllem 6952  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  fsumcom 6966  fsumrev 6967  fsummulc1 6971  fsumcmp 6978  fsumcmpndx2 6980  fsumabs 6981  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag3 7195  fsum0diag4 7196  infxpidmlem5 7499  infxpidmlem7 7501  infxpidmlem8 7502  unitgt 7565  tgss2t 7579  elcls 7646  clsndisj 7648  elcls3 7652  neindisj 7672  lpval 7684  lpsscls 7686  clslp 7689  cncnpi 7712  cncnp 7717  opni2 7805  rnblopn 7814  caussi 7889  bcthlem28 7960  subgabl 8060  nmcnc 8276  sspmval 8326  sspival 8331  sspimsval 8333  sspph 8446  ubthlem6 8465  shelt 9001  shsubclt 9010  shsubcltOLD 9011  chelt 9021  ocorth 9080  shorth 9084  shselt 9193  elspansn3t 9412  elnlfn2t 9769  sumdmdlem2 10253

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain