Theorem sseldd 3227

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

Syntax hints:   → wi 4   ∈ wcel 2201   ⊆ wss 3199

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212

This theorem is referenced by:  disjiun  4084  exmid01  4290  frirrg  4449  ordtri2or2exmid  4671  ontri2orexmidim  4672  riotass  6006  elovimad  6067  tfrcldm  6534  nntr2  6676  eroveu  6800  eroprf  6802  ixpssmapg  6902  findcard2d  7085  findcard2sd  7086  fimax2gtrilemstep  7095  elssdc  7099  eqsndc  7100  undifdc  7121  fisseneq  7132  fidcenumlemrks  7157  fidcenumlemr  7159  fiuni  7182  suplub2ti  7205  ctssdclemn0  7314  acfun  7427  ccfunen  7488  nnppipi  7568  archnqq  7642  prarloclemlt  7718  suplocexprlemrl  7942  suplocexprlemmu  7943  suplocexprlemdisj  7945  suplocexprlemloc  7946  suplocexprlemex  7947  suplocexprlemub  7948  suplocexprlemlub  7949  suplocsrlemb  8031  suplocsrlempr  8032  suplocsrlem  8033  axpre-suploclemres  8126  suprubex  9136  suprzclex  9583  infregelbex  9837  fzssp1  10307  elfzoelz  10387  fzofzp1  10478  fzostep1  10489  zssinfcl  10498  suprzubdc  10502  zsupssdc  10504  suprzcl2dc  10505  frecuzrdgg  10684  frecuzrdgdomlem  10685  frecuzrdgsuctlem  10691  ser3mono  10755  seqf1oglem2a  10786  seqf1oglem2  10788  bcm1k  11028  fimaxq  11097  leisorel  11107  zfz1isolemiso  11109  seq3coll  11112  fun2dmnop0  11120  swrdclg  11240  fimaxre2  11810  summodclem2a  11965  fsum3cvg3  11980  fsumcl2lem  11982  fsum0diaglem  12024  fsumiun  12061  prodmodclem2a  12160  fprodcl2lem  12189  fprodap0  12205  fprodrec  12213  fprodap0f  12220  fprodle  12224  bitsfzolem  12538  bitsfzo  12539  uzwodc  12631  4sqlemffi  12992  ennnfonelemhom  13059  exmidunben  13070  ctiunctlemfo  13083  nninfdclemcl  13092  nninfdclemp1  13094  nninfdclemlt  13095  nninfdclemf1  13096  unbendc  13098  strsetsid  13138  strslssd  13152  gsumpropd2  13499  gsumress  13501  resmhm  13593  mhmima  13597  grpidssd  13682  grpinvssd  13683  mulgnnsubcl  13744  mulgnn0subcl  13745  mulgsubcl  13746  mulgpropdg  13774  submmulg  13776  subg0  13790  subgsubcl  13795  subgsub  13796  subgmulg  13798  issubg4m  13803  nsgconj  13816  ssnmz  13821  ghmnsgima  13878  subgabl  13942  rdivmuldivd  14182  rhmunitinv  14216  subrguss  14274  subrginv  14275  subrgdv  14276  lsselg  14399  islss3  14417  lspsnel3  14443  lsspropdg  14469  rnglidlmcl  14518  znf1o  14689  topssnei  14915  cnprcl2k  14959  cnss1  14979  cnptopresti  14991  cnptoprest  14992  lmres  15001  txopn  15018  txcnp  15024  xmetres2  15132  blin2  15185  blopn  15243  xmettxlem  15262  xmettx  15263  elcncf2  15327  cncfmet  15345  cncfmptc  15349  cncfmptid  15350  negcncf  15358  mulcncflem  15360  cnrehmeocntop  15363  dedekindeulemuub  15370  dedekindeulemlu  15374  suplociccreex  15377  suplociccex  15378  dedekindicclemuub  15379  dedekindicclemlu  15383  dedekindicclemeu  15384  dedekindicclemicc  15385  ivthinclemlopn  15389  ivthinclemuopn  15391  ivthdec  15397  limcimolemlt  15417  cnplimcim  15420  cnplimclemle  15421  cnplimclemr  15422  cnlimci  15426  limccnpcntop  15428  limccnp2lem  15429  limccnp2cntop  15430  dvlemap  15433  dvfgg  15441  dvidsslem  15446  dvconstss  15451  dvcnp2cntop  15452  dvaddxxbr  15454  dvmulxxbr  15455  dvcoapbr  15460  dvcjbr  15461  plyf  15490  plycolemc  15511  dvply2g  15519  reeff1olem  15524  lgsquadlem3  15837  upgrex  15983  upgr1een  16004  subgruhgredgdm  16150  1hegrvtxdg1fi  16189  wlkvtxiedg  16225  wlkvtxiedgg  16226  sssneq  16663