Theorem sseldd 3243

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 3241	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2205   ⊆ wss 3214

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  disjiun  4109  exmid01  4316  frirrg  4476  ordtri2or2exmid  4698  ontri2orexmidim  4699  riotass  6041  elovimad  6102  funsssuppss  6471  suppssfvg  6476  tfrcldm  6607  nntr2  6749  eroveu  6873  eroprf  6875  ixpssmapg  6976  findcard2d  7161  findcard2sd  7162  fimax2gtrilemstep  7171  elssdc  7175  eqsndc  7176  undifdc  7197  fisseneq  7208  fissfi  7229  fidcenumlemrks  7236  fidcenumlemr  7238  fiuni  7278  suplub2ti  7305  ctssdclemn0  7414  acfun  7527  ccfunen  7594  nnppipi  7674  archnqq  7748  prarloclemlt  7824  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  suplocexprlemlub  8055  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axpre-suploclemres  8232  suprubex  9245  suprzclex  9697  infregelbex  9951  fzssp1  10425  elfzoelz  10506  fzofzp1  10597  fzostep1  10608  zssinfcl  10617  suprzubdc  10623  zsupssdc  10625  suprzcl2dc  10626  frecuzrdgg  10805  frecuzrdgdomlem  10806  frecuzrdgsuctlem  10812  ser3mono  10876  seqf1oglem2a  10907  seqf1oglem2  10909  bcm1k  11150  fimaxq  11222  leisorel  11237  zfz1isolemiso  11239  seq3coll  11242  fun2dmnop0  11250  swrdclg  11370  fimaxre2  11940  summodclem2a  12095  fsum3cvg3  12110  fsumcl2lem  12112  fsum0diaglem  12154  fsumiun  12191  prodmodclem2a  12290  fprodcl2lem  12319  fprodap0  12335  fprodrec  12343  fprodap0f  12350  fprodle  12354  bitsfzolem  12668  bitsfzo  12669  uzwodc  12761  4sqlemffi  13122  ballotfilemcdc  13170  ballotfilemsdom  13202  ballotfilemfrceq  13219  ennnfonelemhom  13253  exmidunben  13264  ctiunctlemfo  13277  nninfdclemcl  13286  nninfdclemp1  13288  nninfdclemlt  13289  nninfdclemf1  13290  unbendc  13292  strsetsid  13332  strslssd  13346  gsumpropd2  13659  gsumress  13661  resmhm  13745  mhmima  13749  grpidssd  13834  grpinvssd  13835  mulgnnsubcl  13890  mulgnn0subcl  13891  mulgsubcl  13892  mulgpropdg  13920  submmulg  13922  subg0  13936  subgsubcl  13941  subgsub  13942  subgmulg  13944  issubg4m  13949  nsgconj  13962  ssnmz  13967  ghmnsgima  14024  subgabl  14088  rdivmuldivd  14392  rhmunitinv  14426  subrguss  14485  subrginv  14486  subrgdv  14487  lsselg  14638  islss3  14656  lspsnel3  14682  lsspropdg  14708  rnglidlmcl  14757  znf1o  14928  topssnei  15156  cnprcl2k  15200  cnss1  15220  cnptopresti  15232  cnptoprest  15233  lmres  15242  txopn  15259  txcnp  15265  xmetres2  15373  blin2  15426  blopn  15484  xmettxlem  15503  xmettx  15504  elcncf2  15568  cncfmet  15586  cncfmptc  15590  cncfmptid  15591  negcncf  15599  mulcncflem  15601  cnrehmeocntop  15604  dedekindeulemuub  15611  dedekindeulemlu  15615  suplociccreex  15618  suplociccex  15619  dedekindicclemuub  15620  dedekindicclemlu  15624  dedekindicclemeu  15625  dedekindicclemicc  15626  ivthinclemlopn  15630  ivthinclemuopn  15632  ivthdec  15638  limcimolemlt  15658  cnplimcim  15661  cnplimclemle  15662  cnplimclemr  15663  cnlimci  15667  limccnpcntop  15669  limccnp2lem  15670  limccnp2cntop  15671  dvlemap  15674  dvfgg  15682  dvidsslem  15687  dvconstss  15692  dvcnp2cntop  15693  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  dvcjbr  15702  plyf  15731  plycolemc  15752  dvply2g  15760  reeff1olem  15765  lgsquadlem3  16081  upgrex  16227  upgr1een  16248  subgruhgredgdm  16394  1hegrvtxdg1fi  16433  wlkvtxiedg  16469  wlkvtxiedgg  16470  sssneq  16915