Theorem sseli 3176

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 3174	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2164   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  sselii  3177  sselid  3178  elun1  3327  elun2  3328  finds  4633  finds2  4634  issref  5049  2elresin  5366  fvun1  5624  fvmptssdm  5643  elfvmptrab1  5653  fvimacnvi  5673  elpreima  5678  ofrfval  6141  ofvalg  6142  off  6145  offres  6189  eqopi  6227  op1steq  6234  dfoprab4  6247  f1od2  6290  reldmtpos  6308  smores3  6348  smores2  6349  ctssdccl  7172  pinn  7371  indpi  7404  enq0enq  7493  preqlu  7534  elinp  7536  prop  7537  elnp1st2nd  7538  prarloclem5  7562  cauappcvgprlemladd  7720  peano5nnnn  7954  nnindnn  7955  recn  8007  rexr  8067  peano5nni  8987  nnre  8991  nncn  8992  nnind  9000  nnnn0  9250  nn0re  9252  nn0cn  9253  nn0xnn0  9310  nnz  9339  nn0z  9340  nnq  9701  qcn  9702  rpre  9729  iccshftri  10064  iccshftli  10066  iccdili  10068  icccntri  10070  fzval2  10080  fzelp1  10143  4fvwrd4  10209  elfzo1  10260  expcllem  10624  expcl2lemap  10625  m1expcl2  10635  bcm1k  10834  bcpasc  10840  wrdv  10933  cau3lem  11261  climconst2  11437  fsum3  11533  binomlem  11629  fprodge1  11785  cos12dec  11914  dvdsflip  11996  infssuzcldc  12091  isprm3  12259  phimullem  12366  prmdiveq  12377  structcnvcnv  12637  fvsetsid  12655  ptex  12878  nmzsubg  13283  nmznsg  13286  nzrring  13682  lringnzr  13692  rege0subm  14083  znrrg  14159  tgval2  14230  qtopbasss  14700  dedekindicc  14812  ivthinc  14822  ivthdec  14823  cosz12  14956  cos0pilt1  15028  ioocosf1o  15030  lgsquadlemofi  15233  lgsquadlem1  15234  lgsquadlem2  15235  exmidsbthrlem  15582