Theorem sseli 3093

Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
sseli	⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssel 3091	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

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

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 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  sselii  3094  sseldi  3095  elun1  3243  elun2  3244  finds  4514  finds2  4515  issref  4921  2elresin  5234  fvun1  5487  fvmptssdm  5505  elfvmptrab1  5515  fvimacnvi  5534  elpreima  5539  ofrfval  5990  ofvalg  5991  off  5994  offres  6033  eqopi  6070  op1steq  6077  dfoprab4  6090  f1od2  6132  reldmtpos  6150  smores3  6190  smores2  6191  ctssdccl  6996  pinn  7117  indpi  7150  enq0enq  7239  preqlu  7280  elinp  7282  prop  7283  elnp1st2nd  7284  prarloclem5  7308  cauappcvgprlemladd  7466  peano5nnnn  7700  nnindnn  7701  recn  7753  rexr  7811  peano5nni  8723  nnre  8727  nncn  8728  nnind  8736  nnnn0  8984  nn0re  8986  nn0cn  8987  nn0xnn0  9044  nnz  9073  nn0z  9074  nnq  9425  qcn  9426  rpre  9448  iccshftri  9778  iccshftli  9780  iccdili  9782  icccntri  9784  fzval2  9793  fzelp1  9854  4fvwrd4  9917  elfzo1  9967  expcllem  10304  expcl2lemap  10305  m1expcl2  10315  bcm1k  10506  bcpasc  10512  cau3lem  10886  climconst2  11060  fsum3  11156  binomlem  11252  cos12dec  11474  dvdsflip  11549  infssuzcldc  11644  isprm3  11799  phimullem  11901  structcnvcnv  11975  fvsetsid  11993  tgval2  12220  qtopbasss  12690  dedekindicc  12780  ivthinc  12790  ivthdec  12791  cosz12  12861  exmidsbthrlem  13217