Theorem sseli 3223

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

Syntax hints:   → wi 4   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sselii  3224  sselid  3225  elun1  3374  elun2  3375  elopabr  4377  elopabran  4378  finds  4698  finds2  4699  issref  5119  2elresin  5443  fvun1  5712  fvmptssdm  5731  elfvmptrab1  5741  fvimacnvi  5761  elpreima  5766  ofrfval  6243  ofvalg  6244  off  6247  offres  6296  eqopi  6334  op1steq  6341  dfoprab4  6354  f1od2  6399  reldmtpos  6418  smores3  6458  smores2  6459  ctssdccl  7309  pinn  7528  indpi  7561  enq0enq  7650  preqlu  7691  elinp  7693  prop  7694  elnp1st2nd  7695  prarloclem5  7719  cauappcvgprlemladd  7877  peano5nnnn  8111  nnindnn  8112  recn  8164  rexr  8224  peano5nni  9145  nnre  9149  nncn  9150  nnind  9158  nnnn0  9408  nn0re  9410  nn0cn  9411  nn0xnn0  9468  nnz  9497  nn0z  9498  uzuzle35  9798  nnq  9866  qcn  9867  rpre  9894  iccshftri  10229  iccshftli  10231  iccdili  10233  icccntri  10235  fzval2  10245  fzelp1  10308  4fvwrd4  10374  elfzo1  10429  infssuzcldc  10494  expcllem  10811  expcl2lemap  10812  m1expcl2  10822  bcm1k  11021  bcpasc  11027  wrdv  11128  ccatclab  11170  pfxfv0  11272  pfxfvlsw  11275  cau3lem  11674  climconst2  11851  fsum3  11947  binomlem  12043  fprodge1  12199  cos12dec  12328  dvdsflip  12411  isprm3  12689  phimullem  12796  prmdiveq  12807  structcnvcnv  13097  fvsetsid  13115  ptex  13346  nmzsubg  13796  nmznsg  13799  nzrring  14196  lringnzr  14206  rege0subm  14597  znrrg  14673  tgval2  14774  qtopbasss  15244  dedekindicc  15356  ivthinc  15366  ivthdec  15367  dvply2  15490  cosz12  15503  cos0pilt1  15575  ioocosf1o  15577  mpodvdsmulf1o  15713  fsumdvdsmul  15714  lgsquadlemofi  15804  lgsquadlem1  15805  lgsquadlem2  15806  wlk1walkdom  16209  exmidsbthrlem  16626