Theorem sseldd 3249

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  disjiun  4125  exmid01  4337  frirrg  4497  ordtri2or2exmid  4720  ontri2orexmidim  4721  riotass  6071  elovimad  6132  funsssuppss  6502  suppssfvg  6507  tfrcldm  6638  nntr2  6780  eroveu  6904  eroprf  6906  ixpssmapg  7014  findcard2d  7199  findcard2sd  7200  fimax2gtrilemstep  7209  elssdc  7213  eqsndc  7214  undifdc  7235  fisseneq  7246  fissfi  7267  fidcenumlemrks  7275  fidcenumlemr  7277  fiuni  7317  suplub2ti  7347  ctssdclemn0  7456  acfun  7569  ccfunen  7636  nnppipi  7716  archnqq  7790  prarloclemlt  7866  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  suplocexprlemlub  8097  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axpre-suploclemres  8274  suprubex  9289  ind1  9309  suprzclex  9755  infregelbex  10014  fzssp1  10490  elfzoelz  10571  fzofzp1  10662  fzostep1  10673  zssinfcl  10682  suprzubdc  10688  zsupssdc  10690  suprzcl2dc  10691  frecuzrdgg  10874  frecuzrdgdomlem  10875  frecuzrdgsuctlem  10881  ser3mono  10945  seqf1oglem2a  10976  seqf1oglem2  10978  bcm1k  11220  fimaxq  11292  leisorel  11311  zfz1isolemiso  11313  seq3coll  11316  fun2dmnop0  11324  swrdclg  11444  fimaxre2  12016  fiidxsupcl  12018  summodclem2a  12173  fsum3cvg3  12188  fsumcl2lem  12190  fsum0diaglem  12232  fsumiun  12269  prodmodclem2a  12368  fprodcl2lem  12397  fprodap0  12413  fprodrec  12421  fprodap0f  12428  fprodle  12432  bitsfzolem  12746  bitsfzo  12747  uzwodc  12839  4sqlemffi  13204  ballotfilemcdc  13281  ballotfilemsdom  13313  ballotfilemfrceq  13330  ennnfonelemhom  13364  exmidunben  13375  ctiunctlemfo  13388  nninfdclemcl  13397  nninfdclemp1  13399  nninfdclemlt  13400  nninfdclemf1  13401  unbendc  13403  strsetsid  13443  strslssd  13457  gzsumress  13771  resmhm  13853  mhmima  13857  grpidssd  13940  grpinvssd  13941  mulgnnsubcl  13996  mulgnn0subcl  13997  mulgsubcl  13998  mulgpropdg  14026  submmulg  14028  subg0  14042  subgsubcl  14047  subgsub  14048  subgmulg  14050  issubg4m  14055  nsgconj  14068  ssnmz  14073  ghmnsgima  14130  cntzrcl  14159  cntzssv  14160  cntrsubgnsg  14175  cmnsubm  14202  subgabl  14226  gsummptfidmsplit  14254  rdivmuldivd  14560  rhmunitinv  14594  subrguss  14653  subrginv  14654  subrgdv  14655  lsselg  14807  islss3  14825  ellspsn3  14851  lsspropdg  14877  rnglidlmcl  14926  znf1o  15095  issubassa2  15144  topssnei  15385  cnprcl2k  15429  cnss1  15449  cnptopresti  15461  cnptoprest  15462  lmres  15471  txopn  15488  txcnp  15494  xmetres2  15602  blin2  15655  blopn  15713  xmettxlem  15732  xmettx  15733  elcncf2  15797  cncfmet  15815  cncfmptc  15819  cncfmptid  15820  negcncf  15828  mulcncflem  15830  cnrehmeocntop  15833  dedekindeulemuub  15840  dedekindeulemlu  15844  suplociccreex  15847  suplociccex  15848  dedekindicclemuub  15849  dedekindicclemlu  15853  dedekindicclemeu  15854  dedekindicclemicc  15855  ivthinclemlopn  15859  ivthinclemuopn  15861  ivthdec  15867  limcimolemlt  15887  cnplimcim  15890  cnplimclemle  15891  cnplimclemr  15892  cnlimci  15896  limccnpcntop  15898  limccnp2lem  15899  limccnp2cntop  15900  dvlemap  15903  dvfgg  15911  dvidsslem  15916  dvconstss  15921  dvcnp2cntop  15922  dvaddxxbr  15924  dvmulxxbr  15925  dvcoapbr  15930  dvcjbr  15931  plyf  15960  plycolemc  15981  dvply2g  15989  reeff1olem  15994  lgsquadlem3  16400  upgrex  16546  upgr1een  16567  subgruhgredgdm  16713  1hegrvtxdg1fi  16752  wlkvtxiedg  16788  wlkvtxiedgg  16789  sssneq  17234