Theorem sseldd 3195

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

Syntax hints:   → wi 4   ∈ wcel 2177   ⊆ wss 3167

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3173  df-ss 3180

This theorem is referenced by:  disjiun  4042  exmid01  4246  frirrg  4401  ordtri2or2exmid  4623  ontri2orexmidim  4624  riotass  5934  tfrcldm  6456  nntr2  6596  eroveu  6720  eroprf  6722  ixpssmapg  6822  findcard2d  6995  findcard2sd  6996  fimax2gtrilemstep  7004  undifdc  7028  fisseneq  7038  fidcenumlemrks  7062  fidcenumlemr  7064  fiuni  7087  suplub2ti  7110  ctssdclemn0  7219  acfun  7326  ccfunen  7383  nnppipi  7463  archnqq  7537  prarloclemlt  7613  suplocexprlemrl  7837  suplocexprlemmu  7838  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemex  7842  suplocexprlemub  7843  suplocexprlemlub  7844  suplocsrlemb  7926  suplocsrlempr  7927  suplocsrlem  7928  axpre-suploclemres  8021  suprubex  9031  suprzclex  9478  infregelbex  9726  fzssp1  10196  elfzoelz  10276  fzofzp1  10363  fzostep1  10373  zssinfcl  10382  suprzubdc  10386  zsupssdc  10388  suprzcl2dc  10389  frecuzrdgg  10568  frecuzrdgdomlem  10569  frecuzrdgsuctlem  10575  ser3mono  10639  seqf1oglem2a  10670  seqf1oglem2  10672  bcm1k  10912  fimaxq  10979  leisorel  10989  zfz1isolemiso  10991  seq3coll  10994  fun2dmnop0  10999  swrdclg  11111  fimaxre2  11582  summodclem2a  11736  fsum3cvg3  11751  fsumcl2lem  11753  fsum0diaglem  11795  fsumiun  11832  prodmodclem2a  11931  fprodcl2lem  11960  fprodap0  11976  fprodrec  11984  fprodap0f  11991  fprodle  11995  bitsfzolem  12309  bitsfzo  12310  uzwodc  12402  4sqlemffi  12763  ennnfonelemhom  12830  exmidunben  12841  ctiunctlemfo  12854  nninfdclemcl  12863  nninfdclemp1  12865  nninfdclemlt  12866  nninfdclemf1  12867  unbendc  12869  strsetsid  12909  strslssd  12923  gsumpropd2  13269  gsumress  13271  resmhm  13363  mhmima  13367  grpidssd  13452  grpinvssd  13453  mulgnnsubcl  13514  mulgnn0subcl  13515  mulgsubcl  13516  mulgpropdg  13544  submmulg  13546  subg0  13560  subgsubcl  13565  subgsub  13566  subgmulg  13568  issubg4m  13573  nsgconj  13586  ssnmz  13591  ghmnsgima  13648  subgabl  13712  rdivmuldivd  13950  rhmunitinv  13984  subrguss  14042  subrginv  14043  subrgdv  14044  lsselg  14167  islss3  14185  lspsnel3  14211  lsspropdg  14237  rnglidlmcl  14286  znf1o  14457  topssnei  14678  cnprcl2k  14722  cnss1  14742  cnptopresti  14754  cnptoprest  14755  lmres  14764  txopn  14781  txcnp  14787  xmetres2  14895  blin2  14948  blopn  15006  xmettxlem  15025  xmettx  15026  elcncf2  15090  cncfmet  15108  cncfmptc  15112  cncfmptid  15113  negcncf  15121  mulcncflem  15123  cnrehmeocntop  15126  dedekindeulemuub  15133  dedekindeulemlu  15137  suplociccreex  15140  suplociccex  15141  dedekindicclemuub  15142  dedekindicclemlu  15146  dedekindicclemeu  15147  dedekindicclemicc  15148  ivthinclemlopn  15152  ivthinclemuopn  15154  ivthdec  15160  limcimolemlt  15180  cnplimcim  15183  cnplimclemle  15184  cnplimclemr  15185  cnlimci  15189  limccnpcntop  15191  limccnp2lem  15192  limccnp2cntop  15193  dvlemap  15196  dvfgg  15204  dvidsslem  15209  dvconstss  15214  dvcnp2cntop  15215  dvaddxxbr  15217  dvmulxxbr  15218  dvcoapbr  15223  dvcjbr  15224  plyf  15253  plycolemc  15274  dvply2g  15282  reeff1olem  15287  lgsquadlem3  15600  sssneq  16013