Theorem sselid 3145

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 3143	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  mptrcl  5576  riotacl  5820  riotasbc  5821  elmpocl  6044  ofrval  6068  f1od2  6211  mpoxopn0yelv  6215  tpostpos  6240  smores  6268  supubti  6972  suplubti  6973  prarloclemcalc  7451  rereceu  7838  recriota  7839  rexrd  7956  eqord1  8389  nnred  8878  nncnd  8879  un0addcl  9155  un0mulcl  9156  nnnn0d  9175  nn0red  9176  nn0xnn0d  9194  suprzclex  9297  nn0zd  9319  zred  9321  rpred  9640  ige2m1fz  10053  zmodfzp1  10291  seq3caopr2  10425  expcl2lemap  10475  m1expcl  10486  summodclem2a  11331  zsumdc  11334  clim2prod  11489  ntrivcvgap  11498  prodmodclem2a  11526  zproddc  11529  zsupssdc  11896  lcmn0cl  12009  isprm5lem  12082  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemh  12172  eulerthlemth  12173  prmdivdiv  12178  ennnfonelemg  12345  lmrcl  12944  lmss  12999  upxp  13025  isxms2  13205  iooretopg  13281  tgqioo  13300  limccoap  13400  dvcl  13405  dvidlemap  13413  dvcnp2cntop  13416  lgscl  13668  2sqlem6  13709  2sqlem8  13712  2sqlem9  13713  isomninnlem  14022  trilpolemeq1  14032  trilpolemlt1  14033  iswomninnlem  14041  iswomni0  14043  ismkvnnlem  14044  nconstwlpolemgt0  14055