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  4335  frirrg  4495  ordtri2or2exmid  4718  ontri2orexmidim  4719  riotass  6068  elovimad  6129  funsssuppss  6498  suppssfvg  6503  tfrcldm  6634  nntr2  6776  eroveu  6900  eroprf  6902  ixpssmapg  7010  findcard2d  7195  findcard2sd  7196  fimax2gtrilemstep  7205  elssdc  7209  eqsndc  7210  undifdc  7231  fisseneq  7242  fissfi  7263  fidcenumlemrks  7270  fidcenumlemr  7272  fiuni  7312  suplub2ti  7341  ctssdclemn0  7450  acfun  7563  ccfunen  7630  nnppipi  7710  archnqq  7784  prarloclemlt  7860  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  suplocexprlemlub  8091  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axpre-suploclemres  8268  suprubex  9282  ind1  9301  suprzclex  9746  infregelbex  10000  fzssp1  10475  elfzoelz  10556  fzofzp1  10647  fzostep1  10658  zssinfcl  10667  suprzubdc  10673  zsupssdc  10675  suprzcl2dc  10676  frecuzrdgg  10855  frecuzrdgdomlem  10856  frecuzrdgsuctlem  10862  ser3mono  10926  seqf1oglem2a  10957  seqf1oglem2  10959  bcm1k  11200  fimaxq  11272  leisorel  11291  zfz1isolemiso  11293  seq3coll  11296  fun2dmnop0  11304  swrdclg  11424  fimaxre2  11995  summodclem2a  12150  fsum3cvg3  12165  fsumcl2lem  12167  fsum0diaglem  12209  fsumiun  12246  prodmodclem2a  12345  fprodcl2lem  12374  fprodap0  12390  fprodrec  12398  fprodap0f  12405  fprodle  12409  bitsfzolem  12723  bitsfzo  12724  uzwodc  12816  4sqlemffi  13177  ballotfilemcdc  13225  ballotfilemsdom  13257  ballotfilemfrceq  13274  ennnfonelemhom  13308  exmidunben  13319  ctiunctlemfo  13332  nninfdclemcl  13341  nninfdclemp1  13343  nninfdclemlt  13344  nninfdclemf1  13345  unbendc  13347  strsetsid  13387  strslssd  13401  gzsumress  13714  resmhm  13796  mhmima  13800  grpidssd  13883  grpinvssd  13884  mulgnnsubcl  13939  mulgnn0subcl  13940  mulgsubcl  13941  mulgpropdg  13969  submmulg  13971  subg0  13985  subgsubcl  13990  subgsub  13991  subgmulg  13993  issubg4m  13998  nsgconj  14011  ssnmz  14016  ghmnsgima  14073  cmnsubm  14114  subgabl  14138  rdivmuldivd  14453  rhmunitinv  14487  subrguss  14546  subrginv  14547  subrgdv  14548  lsselg  14700  islss3  14718  ellspsn3  14744  lsspropdg  14770  rnglidlmcl  14819  znf1o  14988  issubassa2  15037  topssnei  15265  cnprcl2k  15309  cnss1  15329  cnptopresti  15341  cnptoprest  15342  lmres  15351  txopn  15368  txcnp  15374  xmetres2  15482  blin2  15535  blopn  15593  xmettxlem  15612  xmettx  15613  elcncf2  15677  cncfmet  15695  cncfmptc  15699  cncfmptid  15700  negcncf  15708  mulcncflem  15710  cnrehmeocntop  15713  dedekindeulemuub  15720  dedekindeulemlu  15724  suplociccreex  15727  suplociccex  15728  dedekindicclemuub  15729  dedekindicclemlu  15733  dedekindicclemeu  15734  dedekindicclemicc  15735  ivthinclemlopn  15739  ivthinclemuopn  15741  ivthdec  15747  limcimolemlt  15767  cnplimcim  15770  cnplimclemle  15771  cnplimclemr  15772  cnlimci  15776  limccnpcntop  15778  limccnp2lem  15779  limccnp2cntop  15780  dvlemap  15783  dvfgg  15791  dvidsslem  15796  dvconstss  15801  dvcnp2cntop  15802  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvcjbr  15811  plyf  15840  plycolemc  15861  dvply2g  15869  reeff1olem  15874  lgsquadlem3  16210  upgrex  16356  upgr1een  16377  subgruhgredgdm  16523  1hegrvtxdg1fi  16562  wlkvtxiedg  16598  wlkvtxiedgg  16599  sssneq  17044