Theorem sselid 3181

Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)

Hypotheses

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵
sselid.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
sselid	⊢ (𝜑 → 𝐶 ∈ 𝐵)

Proof of Theorem sselid

Step	Hyp	Ref	Expression
1		sselid.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		sseli.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	2	sseli 3179	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  mptrcl  5644  riotacl  5892  riotasbc  5893  elmpocl  6118  ofrval  6146  f1od2  6293  mpoxopn0yelv  6297  tpostpos  6322  smores  6350  supubti  7065  suplubti  7066  nninfwlporlemd  7238  nninfwlporlem  7239  nninfwlpoimlemg  7241  nninfwlpoimlemginf  7242  prarloclemcalc  7569  rereceu  7956  recriota  7957  rexrd  8076  eqord1  8510  nnred  9003  nncnd  9004  un0addcl  9282  un0mulcl  9283  nnnn0d  9302  nn0red  9303  nn0xnn0d  9321  suprzclex  9424  nn0zd  9446  zred  9448  rpred  9771  ige2m1fz  10185  zsupssdc  10328  zmodfzp1  10440  seq3caopr2  10585  seqf1oglem1  10611  seqf1oglem2  10612  expcl2lemap  10643  m1expcl  10654  summodclem2a  11546  zsumdc  11549  clim2prod  11704  ntrivcvgap  11713  prodmodclem2a  11741  zproddc  11744  bitsfzolem  12118  nninfctlemfo  12207  lcmn0cl  12236  isprm5lem  12309  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  prmdivdiv  12405  4sqlem13m  12572  4sqlem14  12573  4sqlem17  12576  ennnfonelemg  12620  relelbasov  12740  nmzsubg  13340  conjnmz  13409  conjnmzb  13410  rrgeq0  13821  znf1o  14207  lmrcl  14427  lmss  14482  upxp  14508  isxms2  14688  iooretopg  14764  tgqioo  14791  maxcncf  14851  mincncf  14852  ivthreinc  14881  limccoap  14914  dvcl  14919  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvconstss  14934  dvcnp2cntop  14935  plyaddcl  14990  plymulcl  14991  plysubcl  14992  wilthlem1  15216  sgmval2  15220  mpodvdsmulf1o  15226  fsumdvdsmul  15227  sgmmul  15232  perfectlem2  15236  lgscl  15255  lgsquadlem1  15318  lgsquadlem2  15319  2sqlem6  15361  2sqlem8  15364  2sqlem9  15365  isomninnlem  15674  trilpolemeq1  15684  trilpolemlt1  15685  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696  nconstwlpolemgt0  15708