Theorem sseldd 3238

Description: Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
sseld.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseldd.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
sseldd	⊢ (𝜑 → 𝐶 ∈ 𝐵)

Proof of Theorem sseldd

Step	Hyp	Ref	Expression
1		sseldd.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		sseld.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	2	sseld 3236	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2203   ⊆ wss 3210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  disjiun  4103  exmid01  4310  frirrg  4470  ordtri2or2exmid  4692  ontri2orexmidim  4693  riotass  6032  elovimad  6093  funsssuppss  6457  suppssfvg  6462  tfrcldm  6593  nntr2  6735  eroveu  6859  eroprf  6861  ixpssmapg  6962  findcard2d  7147  findcard2sd  7148  fimax2gtrilemstep  7157  elssdc  7161  eqsndc  7162  undifdc  7183  fisseneq  7194  fissfi  7215  fidcenumlemrks  7222  fidcenumlemr  7224  fiuni  7264  suplub2ti  7291  ctssdclemn0  7400  acfun  7513  ccfunen  7574  nnppipi  7654  archnqq  7728  prarloclemlt  7804  suplocexprlemrl  8028  suplocexprlemmu  8029  suplocexprlemdisj  8031  suplocexprlemloc  8032  suplocexprlemex  8033  suplocexprlemub  8034  suplocexprlemlub  8035  suplocsrlemb  8117  suplocsrlempr  8118  suplocsrlem  8119  axpre-suploclemres  8212  suprubex  9221  suprzclex  9672  infregelbex  9926  fzssp1  10397  elfzoelz  10477  fzofzp1  10568  fzostep1  10579  zssinfcl  10588  suprzubdc  10592  zsupssdc  10594  suprzcl2dc  10595  frecuzrdgg  10774  frecuzrdgdomlem  10775  frecuzrdgsuctlem  10781  ser3mono  10845  seqf1oglem2a  10876  seqf1oglem2  10878  bcm1k  11118  fimaxq  11187  leisorel  11202  zfz1isolemiso  11204  seq3coll  11207  fun2dmnop0  11215  swrdclg  11335  fimaxre2  11905  summodclem2a  12060  fsum3cvg3  12075  fsumcl2lem  12077  fsum0diaglem  12119  fsumiun  12156  prodmodclem2a  12255  fprodcl2lem  12284  fprodap0  12300  fprodrec  12308  fprodap0f  12315  fprodle  12319  bitsfzolem  12633  bitsfzo  12634  uzwodc  12726  4sqlemffi  13087  ennnfonelemhom  13155  exmidunben  13166  ctiunctlemfo  13179  nninfdclemcl  13188  nninfdclemp1  13190  nninfdclemlt  13191  nninfdclemf1  13192  unbendc  13194  strsetsid  13234  strslssd  13248  gsumpropd2  13595  gsumress  13597  resmhm  13689  mhmima  13693  grpidssd  13778  grpinvssd  13779  mulgnnsubcl  13840  mulgnn0subcl  13841  mulgsubcl  13842  mulgpropdg  13870  submmulg  13872  subg0  13886  subgsubcl  13891  subgsub  13892  subgmulg  13894  issubg4m  13899  nsgconj  13912  ssnmz  13917  ghmnsgima  13974  subgabl  14038  rdivmuldivd  14278  rhmunitinv  14312  subrguss  14370  subrginv  14371  subrgdv  14372  lsselg  14496  islss3  14514  lspsnel3  14540  lsspropdg  14566  rnglidlmcl  14615  znf1o  14786  topssnei  15014  cnprcl2k  15058  cnss1  15078  cnptopresti  15090  cnptoprest  15091  lmres  15100  txopn  15117  txcnp  15123  xmetres2  15231  blin2  15284  blopn  15342  xmettxlem  15361  xmettx  15362  elcncf2  15426  cncfmet  15444  cncfmptc  15448  cncfmptid  15449  negcncf  15457  mulcncflem  15459  cnrehmeocntop  15462  dedekindeulemuub  15469  dedekindeulemlu  15473  suplociccreex  15476  suplociccex  15477  dedekindicclemuub  15478  dedekindicclemlu  15482  dedekindicclemeu  15483  dedekindicclemicc  15484  ivthinclemlopn  15488  ivthinclemuopn  15490  ivthdec  15496  limcimolemlt  15516  cnplimcim  15519  cnplimclemle  15520  cnplimclemr  15521  cnlimci  15525  limccnpcntop  15527  limccnp2lem  15528  limccnp2cntop  15529  dvlemap  15532  dvfgg  15540  dvidsslem  15545  dvconstss  15550  dvcnp2cntop  15551  dvaddxxbr  15553  dvmulxxbr  15554  dvcoapbr  15559  dvcjbr  15560  plyf  15589  plycolemc  15610  dvply2g  15618  reeff1olem  15623  lgsquadlem3  15939  upgrex  16085  upgr1een  16106  subgruhgredgdm  16252  1hegrvtxdg1fi  16291  wlkvtxiedg  16327  wlkvtxiedgg  16328  sssneq  16763