Theorem sseldd 3181

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

Syntax hints:   → wi 4   ∈ wcel 2164   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  disjiun  4025  exmid01  4228  frirrg  4382  ordtri2or2exmid  4604  ontri2orexmidim  4605  riotass  5902  tfrcldm  6418  nntr2  6558  eroveu  6682  eroprf  6684  ixpssmapg  6784  findcard2d  6949  findcard2sd  6950  fimax2gtrilemstep  6958  undifdc  6982  fisseneq  6990  fidcenumlemrks  7014  fidcenumlemr  7016  fiuni  7039  suplub2ti  7062  ctssdclemn0  7171  acfun  7269  ccfunen  7326  nnppipi  7405  archnqq  7479  prarloclemlt  7555  suplocexprlemrl  7779  suplocexprlemmu  7780  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemex  7784  suplocexprlemub  7785  suplocexprlemlub  7786  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axpre-suploclemres  7963  suprubex  8972  suprzclex  9418  infregelbex  9666  fzssp1  10136  elfzoelz  10216  fzofzp1  10297  fzostep1  10307  frecuzrdgg  10490  frecuzrdgdomlem  10491  frecuzrdgsuctlem  10497  ser3mono  10561  seqf1oglem2a  10592  seqf1oglem2  10594  bcm1k  10834  fimaxq  10901  leisorel  10911  zfz1isolemiso  10913  seq3coll  10916  fimaxre2  11373  summodclem2a  11527  fsum3cvg3  11542  fsumcl2lem  11544  fsum0diaglem  11586  fsumiun  11623  prodmodclem2a  11722  fprodcl2lem  11751  fprodap0  11767  fprodrec  11775  fprodap0f  11782  fprodle  11786  zssinfcl  12088  suprzubdc  12092  zsupssdc  12094  suprzcl2dc  12095  uzwodc  12177  4sqlemffi  12537  ennnfonelemhom  12575  exmidunben  12586  ctiunctlemfo  12599  nninfdclemcl  12608  nninfdclemp1  12610  nninfdclemlt  12611  nninfdclemf1  12612  unbendc  12614  strsetsid  12654  strslssd  12668  gsumpropd2  12979  gsumress  12981  resmhm  13062  mhmima  13066  grpidssd  13151  grpinvssd  13152  mulgnnsubcl  13207  mulgnn0subcl  13208  mulgsubcl  13209  mulgpropdg  13237  submmulg  13239  subg0  13253  subgsubcl  13258  subgsub  13259  subgmulg  13261  issubg4m  13266  nsgconj  13279  ssnmz  13284  ghmnsgima  13341  subgabl  13405  rdivmuldivd  13643  rhmunitinv  13677  subrguss  13735  subrginv  13736  subrgdv  13737  lsselg  13860  islss3  13878  lspsnel3  13904  lsspropdg  13930  rnglidlmcl  13979  znf1o  14150  topssnei  14341  cnprcl2k  14385  cnss1  14405  cnptopresti  14417  cnptoprest  14418  lmres  14427  txopn  14444  txcnp  14450  xmetres2  14558  blin2  14611  blopn  14669  xmettxlem  14688  xmettx  14689  elcncf2  14753  cncfmet  14771  cncfmptc  14775  cncfmptid  14776  negcncf  14784  mulcncflem  14786  cnrehmeocntop  14789  dedekindeulemuub  14796  dedekindeulemlu  14800  suplociccreex  14803  suplociccex  14804  dedekindicclemuub  14805  dedekindicclemlu  14809  dedekindicclemeu  14810  dedekindicclemicc  14811  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthdec  14823  limcimolemlt  14843  cnplimcim  14846  cnplimclemle  14847  cnplimclemr  14848  cnlimci  14852  limccnpcntop  14854  limccnp2lem  14855  limccnp2cntop  14856  dvlemap  14859  dvfgg  14867  dvidsslem  14872  dvconstss  14877  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  plyf  14916  plycolemc  14936  reeff1olem  14947  lgsquadlem3  15236  sssneq  15562