Theorem sselid 3138

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

Syntax hints:   → wi 4   ∈ wcel 2135   ⊆ wss 3114

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-in 3120  df-ss 3127

This theorem is referenced by:  mptrcl  5565  riotacl  5809  riotasbc  5810  elmpocl  6033  ofrval  6057  f1od2  6197  mpoxopn0yelv  6201  tpostpos  6226  smores  6254  supubti  6958  suplubti  6959  prarloclemcalc  7437  rereceu  7824  recriota  7825  rexrd  7942  eqord1  8375  nnred  8864  nncnd  8865  un0addcl  9141  un0mulcl  9142  nnnn0d  9161  nn0red  9162  nn0xnn0d  9180  suprzclex  9283  nn0zd  9305  zred  9307  rpred  9626  ige2m1fz  10039  zmodfzp1  10277  seq3caopr2  10411  expcl2lemap  10461  m1expcl  10472  summodclem2a  11316  zsumdc  11319  clim2prod  11474  ntrivcvgap  11483  prodmodclem2a  11511  zproddc  11514  zsupssdc  11881  lcmn0cl  11994  isprm5lem  12067  eulerthlemrprm  12155  eulerthlema  12156  eulerthlemh  12157  eulerthlemth  12158  prmdivdiv  12163  ennnfonelemg  12330  lmrcl  12789  lmss  12844  upxp  12870  isxms2  13050  iooretopg  13126  tgqioo  13145  limccoap  13245  dvcl  13250  dvidlemap  13258  dvcnp2cntop  13261  isomninnlem  13802  trilpolemeq1  13812  trilpolemlt1  13813  iswomninnlem  13821  iswomni0  13823  ismkvnnlem  13824  nconstwlpolemgt0  13835