Theorem sseli 3152

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

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  sselii  3153  sselid  3154  elun1  3303  elun2  3304  finds  4600  finds2  4601  issref  5012  2elresin  5328  fvun1  5583  fvmptssdm  5601  elfvmptrab1  5611  fvimacnvi  5631  elpreima  5636  ofrfval  6091  ofvalg  6092  off  6095  offres  6136  eqopi  6173  op1steq  6180  dfoprab4  6193  f1od2  6236  reldmtpos  6254  smores3  6294  smores2  6295  ctssdccl  7110  pinn  7308  indpi  7341  enq0enq  7430  preqlu  7471  elinp  7473  prop  7474  elnp1st2nd  7475  prarloclem5  7499  cauappcvgprlemladd  7657  peano5nnnn  7891  nnindnn  7892  recn  7944  rexr  8003  peano5nni  8922  nnre  8926  nncn  8927  nnind  8935  nnnn0  9183  nn0re  9185  nn0cn  9186  nn0xnn0  9243  nnz  9272  nn0z  9273  nnq  9633  qcn  9634  rpre  9660  iccshftri  9995  iccshftli  9997  iccdili  9999  icccntri  10001  fzval2  10011  fzelp1  10074  4fvwrd4  10140  elfzo1  10190  expcllem  10531  expcl2lemap  10532  m1expcl2  10542  bcm1k  10740  bcpasc  10746  cau3lem  11123  climconst2  11299  fsum3  11395  binomlem  11491  fprodge1  11647  cos12dec  11775  dvdsflip  11857  infssuzcldc  11952  isprm3  12118  phimullem  12225  prmdiveq  12236  structcnvcnv  12478  fvsetsid  12496  ptex  12713  nmzsubg  13070  nmznsg  13073  nzrring  13327  lringnzr  13334  rege0subm  13481  tgval2  13554  qtopbasss  14024  dedekindicc  14114  ivthinc  14124  ivthdec  14125  cosz12  14204  cos0pilt1  14276  ioocosf1o  14278  exmidsbthrlem  14773