Theorem sseldi 3090

Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)

Hypotheses

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵
sseldi.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
sseldi	⊢ (𝜑 → 𝐶 ∈ 𝐵)

Proof of Theorem sseldi

Step	Hyp	Ref	Expression
1		sseldi.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		sseli.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	2	sseli 3088	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 1480   ⊆ wss 3066

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  mptrcl  5496  riotacl  5737  riotasbc  5738  elmpocl  5961  ofrval  5985  f1od2  6125  mpoxopn0yelv  6129  tpostpos  6154  smores  6182  supubti  6879  suplubti  6880  prarloclemcalc  7303  rereceu  7690  recriota  7691  rexrd  7808  eqord1  8238  nnred  8726  nncnd  8727  un0addcl  9003  un0mulcl  9004  nnnn0d  9023  nn0red  9024  nn0xnn0d  9042  suprzclex  9142  nn0zd  9164  zred  9166  rpred  9476  ige2m1fz  9883  zmodfzp1  10114  seq3caopr2  10248  expcl2lemap  10298  m1expcl  10309  summodclem2a  11143  zsumdc  11146  clim2prod  11301  ntrivcvgap  11310  lcmn0cl  11738  ennnfonelemg  11905  lmrcl  12349  lmss  12404  upxp  12430  isxms2  12610  iooretopg  12686  tgqioo  12705  limccoap  12805  dvcl  12810  dvidlemap  12818  dvcnp2cntop  12821  isomninnlem  13214  trilpolemeq1  13222  trilpolemlt1  13223