Theorem sseldd 3171

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

Syntax hints:   → wi 4   ∈ wcel 2160   ⊆ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  disjiun  4013  exmid01  4216  frirrg  4368  ordtri2or2exmid  4588  ontri2orexmidim  4589  riotass  5879  tfrcldm  6388  nntr2  6528  eroveu  6652  eroprf  6654  ixpssmapg  6754  findcard2d  6919  findcard2sd  6920  fimax2gtrilemstep  6928  undifdc  6952  fisseneq  6960  fidcenumlemrks  6982  fidcenumlemr  6984  fiuni  7007  suplub2ti  7030  ctssdclemn0  7139  acfun  7236  ccfunen  7293  nnppipi  7372  archnqq  7446  prarloclemlt  7522  suplocexprlemrl  7746  suplocexprlemmu  7747  suplocexprlemdisj  7749  suplocexprlemloc  7750  suplocexprlemex  7751  suplocexprlemub  7752  suplocexprlemlub  7753  suplocsrlemb  7835  suplocsrlempr  7836  suplocsrlem  7837  axpre-suploclemres  7930  suprubex  8938  suprzclex  9381  infregelbex  9628  fzssp1  10097  elfzoelz  10177  fzofzp1  10257  fzostep1  10267  frecuzrdgg  10447  frecuzrdgdomlem  10448  frecuzrdgsuctlem  10454  ser3mono  10509  bcm1k  10772  fimaxq  10839  leisorel  10849  zfz1isolemiso  10851  seq3coll  10854  fimaxre2  11267  summodclem2a  11421  fsum3cvg3  11436  fsumcl2lem  11438  fsum0diaglem  11480  fsumiun  11517  prodmodclem2a  11616  fprodcl2lem  11645  fprodap0  11661  fprodrec  11669  fprodap0f  11676  fprodle  11680  zssinfcl  11981  suprzubdc  11985  zsupssdc  11987  suprzcl2dc  11988  uzwodc  12070  4sqlemffi  12428  ennnfonelemhom  12466  exmidunben  12477  ctiunctlemfo  12490  nninfdclemcl  12499  nninfdclemp1  12501  nninfdclemlt  12502  nninfdclemf1  12503  unbendc  12505  strsetsid  12545  strslssd  12559  resmhm  12939  mhmima  12943  grpidssd  13020  grpinvssd  13021  mulgnnsubcl  13074  mulgnn0subcl  13075  mulgsubcl  13076  mulgpropdg  13104  subg0  13119  subgsubcl  13124  subgsub  13125  subgmulg  13127  issubg4m  13132  nsgconj  13145  ssnmz  13150  ghmnsgima  13207  subgabl  13269  rdivmuldivd  13494  rhmunitinv  13528  subrguss  13583  subrginv  13584  subrgdv  13585  lsselg  13677  islss3  13695  lspsnel3  13721  lsspropdg  13747  rnglidlmcl  13796  topssnei  14122  cnprcl2k  14166  cnss1  14186  cnptopresti  14198  cnptoprest  14199  lmres  14208  txopn  14225  txcnp  14231  xmetres2  14339  blin2  14392  blopn  14450  xmettxlem  14469  xmettx  14470  elcncf2  14521  cncfmet  14539  cncfmptc  14542  cncfmptid  14543  negcncf  14548  mulcncflem  14550  cnrehmeocntop  14553  dedekindeulemuub  14555  dedekindeulemlu  14559  suplociccreex  14562  suplociccex  14563  dedekindicclemuub  14564  dedekindicclemlu  14568  dedekindicclemeu  14569  dedekindicclemicc  14570  ivthinclemlopn  14574  ivthinclemuopn  14576  ivthdec  14582  limcimolemlt  14593  cnplimcim  14596  cnplimclemle  14597  cnplimclemr  14598  cnlimci  14602  limccnpcntop  14604  limccnp2lem  14605  limccnp2cntop  14606  dvlemap  14609  dvfgg  14617  dvcnp2cntop  14623  dvaddxxbr  14625  dvmulxxbr  14626  dvcoapbr  14631  dvcjbr  14632  reeff1olem  14652  sssneq  15213