Theorem sselid 3246

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  mptrcl  5791  fnfvimad  5957  riotacl  6057  riotasbc  6058  elmpocl  6287  ofrval  6317  f1od2  6475  elmpom  6478  mpoxopn0yelv  6515  tpostpos  6540  smores  6568  2omap  7324  supubti  7345  suplubti  7346  nninfwlporlemd  7518  nninfwlporlem  7519  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  prarloclemcalc  7875  rereceu  8262  recriota  8263  rexrd  8381  eqord1  8818  nnred  9326  nncnd  9327  un0addcl  9607  un0mulcl  9608  nnnn0d  9629  nn0red  9630  nn0xnn0d  9648  suprzclex  9754  nn0zd  9776  zred  9778  rpred  10113  ige2m1fz  10533  zsupssdc  10689  zmodfzp1  10805  seq3caopr2  10950  seqf1oglem1  10976  seqf1oglem2  10977  expcl2lemap  11008  m1expcl  11019  ccatrn  11398  wrdind  11515  wrd2ind  11516  summodclem2a  12172  zsumdc  12175  clim2prod  12330  ntrivcvgap  12339  prodmodclem2a  12367  zproddc  12370  bitsfzolem  12745  nninfctlemfo  12841  lcmn0cl  12870  isprm5lem  12944  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  prmdivdiv  13043  4sqlem13m  13210  4sqlem14  13211  4sqlem17  13214  ballotfilem2  13285  ballotfilemfrci  13328  ennnfonelemg  13351  relelbasov  13473  nmzsubg  14071  conjnmz  14140  conjnmzb  14141  cntzsgrpcl  14166  cntzsubm  14169  cntzsubg  14170  rrgeq0  14681  znf1o  15094  psrbagconf1o  15177  psrass1filem  15186  psrdifi  15211  psrdirfi  15212  mplelf  15230  mplsubgfilemcl  15232  mpladd  15237  mplnegfi  15238  lmrcl  15435  lmss  15489  upxp  15515  isxms2  15695  iooretopg  15771  tgqioo  15798  maxcncf  15858  mincncf  15859  ivthreinc  15888  limccoap  15921  dvcl  15926  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvconstss  15941  dvcnp2cntop  15942  plyaddcl  15997  plymulcl  15998  plysubcl  15999  pellexlem3  16248  wilthlem1  16249  sgmval2  16270  mpodvdsmulf1o  16301  fsumdvdsmul  16302  sgmmul  16307  perfectlem2  16317  lgscl  16355  lgsquadlem1  16418  lgsquadlem2  16419  2sqlem6  16461  2sqlem8  16464  2sqlem9  16465  upgrss  16562  usgrss  16640  wlkres  16842  trlreslem  16852  idjudju  17269  isomninnlem  17302  trilpolemeq1  17313  trilpolemlt1  17314  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326  nconstwlpolemgt0  17338