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  7015  findcard2d  7200  findcard2sd  7201  fimax2gtrilemstep  7210  elssdc  7214  eqsndc  7215  undifdc  7236  fisseneq  7247  fissfi  7268  fidcenumlemrks  7276  fidcenumlemr  7278  fiuni  7318  suplub2ti  7348  ctssdclemn0  7457  acfun  7570  ccfunen  7637  nnppipi  7717  archnqq  7791  prarloclemlt  7867  suplocexprlemrl  8091  suplocexprlemmu  8092  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemex  8096  suplocexprlemub  8097  suplocexprlemlub  8098  suplocsrlemb  8180  suplocsrlempr  8181  suplocsrlem  8182  axpre-suploclemres  8275  suprubex  9290  ind1  9310  suprzclex  9756  infregelbex  10015  fzssp1  10491  elfzoelz  10572  fzofzp1  10663  fzostep1  10674  zssinfcl  10683  suprzubdc  10689  zsupssdc  10691  suprzcl2dc  10692  frecuzrdgg  10875  frecuzrdgdomlem  10876  frecuzrdgsuctlem  10882  ser3mono  10946  seqf1oglem2a  10977  seqf1oglem2  10979  bcm1k  11221  fimaxq  11293  leisorel  11312  zfz1isolemiso  11314  seq3coll  11317  fun2dmnop0  11325  swrdclg  11445  fimaxre2  12017  fiidxsupcl  12019  summodclem2a  12174  fsum3cvg3  12189  fsumcl2lem  12191  fsum0diaglem  12233  fsumiun  12270  prodmodclem2a  12369  fprodcl2lem  12398  fprodap0  12414  fprodrec  12422  fprodap0f  12429  fprodle  12433  bitsfzolem  12747  bitsfzo  12748  uzwodc  12840  4sqlemffi  13205  ballotfilemcdc  13282  ballotfilemsdom  13314  ballotfilemfrceq  13331  ennnfonelemhom  13365  exmidunben  13376  ctiunctlemfo  13389  nninfdclemcl  13398  nninfdclemp1  13400  nninfdclemlt  13401  nninfdclemf1  13402  unbendc  13404  strsetsid  13444  strslssd  13458  gzsumress  13772  resmhm  13854  mhmima  13858  grpidssd  13941  grpinvssd  13942  mulgnnsubcl  13997  mulgnn0subcl  13998  mulgsubcl  13999  mulgpropdg  14027  submmulg  14029  subg0  14043  subgsubcl  14048  subgsub  14049  subgmulg  14051  issubg4m  14056  nsgconj  14069  ssnmz  14074  ghmnsgima  14131  cntzrcl  14160  cntzssv  14161  cntrsubgnsg  14176  cmnsubm  14203  subgabl  14227  gsummptfidmsplit  14255  rdivmuldivd  14561  rhmunitinv  14595  subrguss  14654  subrginv  14655  subrgdv  14656  lsselg  14808  islss3  14826  ellspsn3  14852  lsspropdg  14878  rnglidlmcl  14927  znf1o  15096  issubassa2  15145  topssnei  15400  cnprcl2k  15444  cnss1  15464  cnptopresti  15476  cnptoprest  15477  lmres  15486  txopn  15503  txcnp  15509  xmetres2  15617  blin2  15670  blopn  15728  xmettxlem  15747  xmettx  15748  elcncf2  15812  cncfmet  15830  cncfmptc  15834  cncfmptid  15835  negcncf  15843  mulcncflem  15845  cnrehmeocntop  15848  dedekindeulemuub  15855  dedekindeulemlu  15859  suplociccreex  15862  suplociccex  15863  dedekindicclemuub  15864  dedekindicclemlu  15868  dedekindicclemeu  15869  dedekindicclemicc  15870  ivthinclemlopn  15874  ivthinclemuopn  15876  ivthdec  15882  limcimolemlt  15902  cnplimcim  15905  cnplimclemle  15906  cnplimclemr  15907  cnlimci  15911  limccnpcntop  15913  limccnp2lem  15914  limccnp2cntop  15915  dvlemap  15918  dvfgg  15926  dvidsslem  15931  dvconstss  15936  dvcnp2cntop  15937  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  dvcjbr  15946  plyf  15975  plycolemc  15996  dvply2g  16004  reeff1olem  16009  lgsquadlem3  16415  upgrex  16561  upgr1een  16582  subgruhgredgdm  16728  1hegrvtxdg1fi  16767  wlkvtxiedg  16803  wlkvtxiedgg  16804  sssneq  17249