Theorem sselid 3236

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

Syntax hints:   → wi 4   ∈ wcel 2203   ⊆ wss 3211

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  mptrcl  5760  fnfvimad  5922  riotacl  6019  riotasbc  6020  elmpocl  6249  ofrval  6277  f1od2  6431  elmpom  6434  mpoxopn0yelv  6470  tpostpos  6495  smores  6523  2omap  7269  supubti  7290  suplubti  7291  nninfwlporlemd  7463  nninfwlporlem  7464  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  prarloclemcalc  7817  rereceu  8204  recriota  8205  rexrd  8323  eqord1  8757  nnred  9250  nncnd  9251  un0addcl  9529  un0mulcl  9530  nnnn0d  9553  nn0red  9554  nn0xnn0d  9572  suprzclex  9676  nn0zd  9698  zred  9700  rpred  10029  ige2m1fz  10444  zsupssdc  10598  zmodfzp1  10710  seq3caopr2  10855  seqf1oglem1  10881  seqf1oglem2  10882  expcl2lemap  10913  m1expcl  10924  ccatrn  11297  wrdind  11414  wrd2ind  11415  summodclem2a  12067  zsumdc  12070  clim2prod  12225  ntrivcvgap  12234  prodmodclem2a  12262  zproddc  12265  bitsfzolem  12640  nninfctlemfo  12736  lcmn0cl  12765  isprm5lem  12838  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  prmdivdiv  12934  4sqlem13m  13101  4sqlem14  13102  4sqlem17  13105  ballotfilem2  13142  ennnfonelemg  13154  relelbasov  13275  nmzsubg  13927  conjnmz  13996  conjnmzb  13997  rrgeq0  14410  znf1o  14799  psrbagconf1o  14828  mplelf  14852  mplsubgfilemcl  14854  mplsubgfileminv  14855  mpladd  14859  mplnegfi  14860  lmrcl  15057  lmss  15111  upxp  15137  isxms2  15317  iooretopg  15393  tgqioo  15420  maxcncf  15480  mincncf  15481  ivthreinc  15510  limccoap  15543  dvcl  15548  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvconstss  15563  dvcnp2cntop  15564  plyaddcl  15619  plymulcl  15620  plysubcl  15621  pellexlem3  15847  wilthlem1  15848  sgmval2  15852  mpodvdsmulf1o  15858  fsumdvdsmul  15859  sgmmul  15864  perfectlem2  15868  lgscl  15887  lgsquadlem1  15950  lgsquadlem2  15951  2sqlem6  15993  2sqlem8  15996  2sqlem9  15997  upgrss  16094  usgrss  16172  wlkres  16374  trlreslem  16384  isomninnlem  16814  trilpolemeq1  16824  trilpolemlt1  16825  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837  nconstwlpolemgt0  16850