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  6244  ofvalg  6245  off  6248  offres  6297  eqopi  6335  op1steq  6342  dfoprab4  6355  f1od2  6400  reldmtpos  6419  smores3  6459  smores2  6460  ctssdccl  7310  pinn  7529  indpi  7562  enq0enq  7651  preqlu  7692  elinp  7694  prop  7695  elnp1st2nd  7696  prarloclem5  7720  cauappcvgprlemladd  7878  peano5nnnn  8112  nnindnn  8113  recn  8165  rexr  8225  peano5nni  9146  nnre  9150  nncn  9151  nnind  9159  nnnn0  9409  nn0re  9411  nn0cn  9412  nn0xnn0  9469  nnz  9498  nn0z  9499  uzuzle35  9799  nnq  9867  qcn  9868  rpre  9895  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  fzval2  10246  fzelp1  10309  4fvwrd4  10375  elfzo1  10431  infssuzcldc  10496  expcllem  10813  expcl2lemap  10814  m1expcl2  10824  bcm1k  11023  bcpasc  11029  wrdv  11133  ccatclab  11175  pfxfv0  11277  pfxfvlsw  11280  cau3lem  11679  climconst2  11856  fsum3  11953  binomlem  12049  fprodge1  12205  cos12dec  12334  dvdsflip  12417  isprm3  12695  phimullem  12802  prmdiveq  12813  structcnvcnv  13103  fvsetsid  13121  ptex  13352  nmzsubg  13802  nmznsg  13805  nzrring  14203  lringnzr  14213  rege0subm  14604  znrrg  14680  tgval2  14781  qtopbasss  15251  dedekindicc  15363  ivthinc  15373  ivthdec  15374  dvply2  15497  cosz12  15510  cos0pilt1  15582  ioocosf1o  15584  mpodvdsmulf1o  15720  fsumdvdsmul  15721  lgsquadlemofi  15811  lgsquadlem1  15812  lgsquadlem2  15813  wlk1walkdom  16216  exmidsbthrlem  16652