Theorem sseldd 3157

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

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  disjiun  3999  exmid01  4199  frirrg  4351  ordtri2or2exmid  4571  ontri2orexmidim  4572  riotass  5858  tfrcldm  6364  nntr2  6504  eroveu  6626  eroprf  6628  ixpssmapg  6728  findcard2d  6891  findcard2sd  6892  fimax2gtrilemstep  6900  undifdc  6923  fisseneq  6931  fidcenumlemrks  6952  fidcenumlemr  6954  fiuni  6977  suplub2ti  7000  ctssdclemn0  7109  acfun  7206  ccfunen  7263  nnppipi  7342  archnqq  7416  prarloclemlt  7492  suplocexprlemrl  7716  suplocexprlemmu  7717  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemex  7721  suplocexprlemub  7722  suplocexprlemlub  7723  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  axpre-suploclemres  7900  suprubex  8908  suprzclex  9351  infregelbex  9598  fzssp1  10067  elfzoelz  10147  fzofzp1  10227  fzostep1  10237  frecuzrdgg  10416  frecuzrdgdomlem  10417  frecuzrdgsuctlem  10423  ser3mono  10478  bcm1k  10740  fimaxq  10807  leisorel  10817  zfz1isolemiso  10819  seq3coll  10822  fimaxre2  11235  summodclem2a  11389  fsum3cvg3  11404  fsumcl2lem  11406  fsum0diaglem  11448  fsumiun  11485  prodmodclem2a  11584  fprodcl2lem  11613  fprodap0  11629  fprodrec  11637  fprodap0f  11644  fprodle  11648  zssinfcl  11949  suprzubdc  11953  zsupssdc  11955  suprzcl2dc  11956  uzwodc  12038  ennnfonelemhom  12416  exmidunben  12427  ctiunctlemfo  12440  nninfdclemcl  12449  nninfdclemp1  12451  nninfdclemlt  12452  nninfdclemf1  12453  unbendc  12455  strsetsid  12495  strslssd  12509  mhmima  12875  grpidssd  12946  grpinvssd  12947  mulgnnsubcl  12995  mulgnn0subcl  12996  mulgsubcl  12997  mulgpropdg  13025  subg0  13040  subgsubcl  13045  subgsub  13046  subgmulg  13048  issubg4m  13053  nsgconj  13066  ssnmz  13071  rdivmuldivd  13313  subrguss  13357  subrginv  13358  subrgdv  13359  topssnei  13665  cnprcl2k  13709  cnss1  13729  cnptopresti  13741  cnptoprest  13742  lmres  13751  txopn  13768  txcnp  13774  xmetres2  13882  blin2  13935  blopn  13993  xmettxlem  14012  xmettx  14013  elcncf2  14064  cncfmet  14082  cncfmptc  14085  cncfmptid  14086  negcncf  14091  mulcncflem  14093  cnrehmeocntop  14096  dedekindeulemuub  14098  dedekindeulemlu  14102  suplociccreex  14105  suplociccex  14106  dedekindicclemuub  14107  dedekindicclemlu  14111  dedekindicclemeu  14112  dedekindicclemicc  14113  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthdec  14125  limcimolemlt  14136  cnplimcim  14139  cnplimclemle  14140  cnplimclemr  14141  cnlimci  14145  limccnpcntop  14147  limccnp2lem  14148  limccnp2cntop  14149  dvlemap  14152  dvfgg  14160  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  reeff1olem  14195  sssneq  14754