Theorem sselid 3155

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

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  mptrcl  5600  riotacl  5847  riotasbc  5848  elmpocl  6071  ofrval  6095  f1od2  6238  mpoxopn0yelv  6242  tpostpos  6267  smores  6295  supubti  7000  suplubti  7001  nninfwlporlemd  7172  nninfwlporlem  7173  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  prarloclemcalc  7503  rereceu  7890  recriota  7891  rexrd  8009  eqord1  8442  nnred  8934  nncnd  8935  un0addcl  9211  un0mulcl  9212  nnnn0d  9231  nn0red  9232  nn0xnn0d  9250  suprzclex  9353  nn0zd  9375  zred  9377  rpred  9698  ige2m1fz  10112  zmodfzp1  10350  seq3caopr2  10484  expcl2lemap  10534  m1expcl  10545  summodclem2a  11391  zsumdc  11394  clim2prod  11549  ntrivcvgap  11558  prodmodclem2a  11586  zproddc  11589  zsupssdc  11957  lcmn0cl  12070  isprm5lem  12143  eulerthlemrprm  12231  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  prmdivdiv  12239  ennnfonelemg  12406  nmzsubg  13075  lmrcl  13730  lmss  13785  upxp  13811  isxms2  13991  iooretopg  14067  tgqioo  14086  limccoap  14186  dvcl  14191  dvidlemap  14199  dvcnp2cntop  14202  lgscl  14454  2sqlem6  14506  2sqlem8  14509  2sqlem9  14510  isomninnlem  14817  trilpolemeq1  14827  trilpolemlt1  14828  iswomninnlem  14836  iswomni0  14838  ismkvnnlem  14839  nconstwlpolemgt0  14851