Theorem sseli 3143

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  sselii  3144  sselid  3145  elun1  3294  elun2  3295  finds  4584  finds2  4585  issref  4993  2elresin  5309  fvun1  5562  fvmptssdm  5580  elfvmptrab1  5590  fvimacnvi  5610  elpreima  5615  ofrfval  6069  ofvalg  6070  off  6073  offres  6114  eqopi  6151  op1steq  6158  dfoprab4  6171  f1od2  6214  reldmtpos  6232  smores3  6272  smores2  6273  ctssdccl  7088  pinn  7271  indpi  7304  enq0enq  7393  preqlu  7434  elinp  7436  prop  7437  elnp1st2nd  7438  prarloclem5  7462  cauappcvgprlemladd  7620  peano5nnnn  7854  nnindnn  7855  recn  7907  rexr  7965  peano5nni  8881  nnre  8885  nncn  8886  nnind  8894  nnnn0  9142  nn0re  9144  nn0cn  9145  nn0xnn0  9202  nnz  9231  nn0z  9232  nnq  9592  qcn  9593  rpre  9617  iccshftri  9952  iccshftli  9954  iccdili  9956  icccntri  9958  fzval2  9968  fzelp1  10030  4fvwrd4  10096  elfzo1  10146  expcllem  10487  expcl2lemap  10488  m1expcl2  10498  bcm1k  10694  bcpasc  10700  cau3lem  11078  climconst2  11254  fsum3  11350  binomlem  11446  fprodge1  11602  cos12dec  11730  dvdsflip  11811  infssuzcldc  11906  isprm3  12072  phimullem  12179  prmdiveq  12190  structcnvcnv  12432  fvsetsid  12450  tgval2  12845  qtopbasss  13315  dedekindicc  13405  ivthinc  13415  ivthdec  13416  cosz12  13495  cos0pilt1  13567  ioocosf1o  13569  exmidsbthrlem  14054