Theorem sseldd 3148

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  disjiun  3984  exmid01  4184  frirrg  4335  ordtri2or2exmid  4555  ontri2orexmidim  4556  riotass  5836  tfrcldm  6342  nntr2  6482  eroveu  6604  eroprf  6606  ixpssmapg  6706  findcard2d  6869  findcard2sd  6870  fimax2gtrilemstep  6878  undifdc  6901  fisseneq  6909  fidcenumlemrks  6930  fidcenumlemr  6932  fiuni  6955  suplub2ti  6978  ctssdclemn0  7087  acfun  7184  ccfunen  7226  nnppipi  7305  archnqq  7379  prarloclemlt  7455  suplocexprlemrl  7679  suplocexprlemmu  7680  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemex  7684  suplocexprlemub  7685  suplocexprlemlub  7686  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axpre-suploclemres  7863  suprubex  8867  suprzclex  9310  infregelbex  9557  fzssp1  10023  elfzoelz  10103  fzofzp1  10183  fzostep1  10193  frecuzrdgg  10372  frecuzrdgdomlem  10373  frecuzrdgsuctlem  10379  ser3mono  10434  bcm1k  10694  fimaxq  10762  leisorel  10772  zfz1isolemiso  10774  seq3coll  10777  fimaxre2  11190  summodclem2a  11344  fsum3cvg3  11359  fsumcl2lem  11361  fsum0diaglem  11403  fsumiun  11440  prodmodclem2a  11539  fprodcl2lem  11568  fprodap0  11584  fprodrec  11592  fprodap0f  11599  fprodle  11603  zssinfcl  11903  suprzubdc  11907  zsupssdc  11909  suprzcl2dc  11910  uzwodc  11992  ennnfonelemhom  12370  exmidunben  12381  ctiunctlemfo  12394  nninfdclemcl  12403  nninfdclemp1  12405  nninfdclemlt  12406  nninfdclemf1  12407  unbendc  12409  strsetsid  12449  strslssd  12462  mhmima  12706  topssnei  12956  cnprcl2k  13000  cnss1  13020  cnptopresti  13032  cnptoprest  13033  lmres  13042  txopn  13059  txcnp  13065  xmetres2  13173  blin2  13226  blopn  13284  xmettxlem  13303  xmettx  13304  elcncf2  13355  cncfmet  13373  cncfmptc  13376  cncfmptid  13377  negcncf  13382  mulcncflem  13384  cnrehmeocntop  13387  dedekindeulemuub  13389  dedekindeulemlu  13393  suplociccreex  13396  suplociccex  13397  dedekindicclemuub  13398  dedekindicclemlu  13402  dedekindicclemeu  13403  dedekindicclemicc  13404  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthdec  13416  limcimolemlt  13427  cnplimcim  13430  cnplimclemle  13431  cnplimclemr  13432  cnlimci  13436  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  dvlemap  13443  dvfgg  13451  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  reeff1olem  13486  sssneq  14035