Theorem sseldd 3241

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

Syntax hints:   → wi 4   ∈ wcel 2205   ⊆ wss 3213

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  disjiun  4106  exmid01  4313  frirrg  4473  ordtri2or2exmid  4695  ontri2orexmidim  4696  riotass  6035  elovimad  6096  funsssuppss  6460  suppssfvg  6465  tfrcldm  6596  nntr2  6738  eroveu  6862  eroprf  6864  ixpssmapg  6965  findcard2d  7150  findcard2sd  7151  fimax2gtrilemstep  7160  elssdc  7164  eqsndc  7165  undifdc  7186  fisseneq  7197  fissfi  7218  fidcenumlemrks  7225  fidcenumlemr  7227  fiuni  7267  suplub2ti  7294  ctssdclemn0  7403  acfun  7516  ccfunen  7583  nnppipi  7663  archnqq  7737  prarloclemlt  7813  suplocexprlemrl  8037  suplocexprlemmu  8038  suplocexprlemdisj  8040  suplocexprlemloc  8041  suplocexprlemex  8042  suplocexprlemub  8043  suplocexprlemlub  8044  suplocsrlemb  8126  suplocsrlempr  8127  suplocsrlem  8128  axpre-suploclemres  8221  suprubex  9230  suprzclex  9682  infregelbex  9936  fzssp1  10407  elfzoelz  10488  fzofzp1  10579  fzostep1  10590  zssinfcl  10599  suprzubdc  10603  zsupssdc  10605  suprzcl2dc  10606  frecuzrdgg  10785  frecuzrdgdomlem  10786  frecuzrdgsuctlem  10792  ser3mono  10856  seqf1oglem2a  10887  seqf1oglem2  10889  bcm1k  11130  fimaxq  11202  leisorel  11217  zfz1isolemiso  11219  seq3coll  11222  fun2dmnop0  11230  swrdclg  11350  fimaxre2  11920  summodclem2a  12075  fsum3cvg3  12090  fsumcl2lem  12092  fsum0diaglem  12134  fsumiun  12171  prodmodclem2a  12270  fprodcl2lem  12299  fprodap0  12315  fprodrec  12323  fprodap0f  12330  fprodle  12334  bitsfzolem  12648  bitsfzo  12649  uzwodc  12741  4sqlemffi  13102  ballotfilemcdc  13150  ennnfonelemhom  13187  exmidunben  13198  ctiunctlemfo  13211  nninfdclemcl  13220  nninfdclemp1  13222  nninfdclemlt  13223  nninfdclemf1  13224  unbendc  13226  strsetsid  13266  strslssd  13280  gsumpropd2  13627  gsumress  13629  resmhm  13721  mhmima  13725  grpidssd  13810  grpinvssd  13811  mulgnnsubcl  13872  mulgnn0subcl  13873  mulgsubcl  13874  mulgpropdg  13902  submmulg  13904  subg0  13918  subgsubcl  13923  subgsub  13924  subgmulg  13926  issubg4m  13931  nsgconj  13944  ssnmz  13949  ghmnsgima  14006  subgabl  14070  rdivmuldivd  14311  rhmunitinv  14345  subrguss  14404  subrginv  14405  subrgdv  14406  lsselg  14558  islss3  14576  lspsnel3  14602  lsspropdg  14628  rnglidlmcl  14677  znf1o  14848  topssnei  15076  cnprcl2k  15120  cnss1  15140  cnptopresti  15152  cnptoprest  15153  lmres  15162  txopn  15179  txcnp  15185  xmetres2  15293  blin2  15346  blopn  15404  xmettxlem  15423  xmettx  15424  elcncf2  15488  cncfmet  15506  cncfmptc  15510  cncfmptid  15511  negcncf  15519  mulcncflem  15521  cnrehmeocntop  15524  dedekindeulemuub  15531  dedekindeulemlu  15535  suplociccreex  15538  suplociccex  15539  dedekindicclemuub  15540  dedekindicclemlu  15544  dedekindicclemeu  15545  dedekindicclemicc  15546  ivthinclemlopn  15550  ivthinclemuopn  15552  ivthdec  15558  limcimolemlt  15578  cnplimcim  15581  cnplimclemle  15582  cnplimclemr  15583  cnlimci  15587  limccnpcntop  15589  limccnp2lem  15590  limccnp2cntop  15591  dvlemap  15594  dvfgg  15602  dvidsslem  15607  dvconstss  15612  dvcnp2cntop  15613  dvaddxxbr  15615  dvmulxxbr  15616  dvcoapbr  15621  dvcjbr  15622  plyf  15651  plycolemc  15672  dvply2g  15680  reeff1olem  15685  lgsquadlem3  16001  upgrex  16147  upgr1een  16168  subgruhgredgdm  16314  1hegrvtxdg1fi  16353  wlkvtxiedg  16389  wlkvtxiedgg  16390  sssneq  16825