Theorem sseli 3221

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

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sselii  3222  sselid  3223  elun1  3372  elun2  3373  elopabr  4375  elopabran  4376  finds  4696  finds2  4697  issref  5117  2elresin  5440  fvun1  5708  fvmptssdm  5727  elfvmptrab1  5737  fvimacnvi  5757  elpreima  5762  ofrfval  6239  ofvalg  6240  off  6243  offres  6292  eqopi  6330  op1steq  6337  dfoprab4  6350  f1od2  6395  reldmtpos  6414  smores3  6454  smores2  6455  ctssdccl  7301  pinn  7519  indpi  7552  enq0enq  7641  preqlu  7682  elinp  7684  prop  7685  elnp1st2nd  7686  prarloclem5  7710  cauappcvgprlemladd  7868  peano5nnnn  8102  nnindnn  8103  recn  8155  rexr  8215  peano5nni  9136  nnre  9140  nncn  9141  nnind  9149  nnnn0  9399  nn0re  9401  nn0cn  9402  nn0xnn0  9459  nnz  9488  nn0z  9489  uzuzle35  9789  nnq  9857  qcn  9858  rpre  9885  iccshftri  10220  iccshftli  10222  iccdili  10224  icccntri  10226  fzval2  10236  fzelp1  10299  4fvwrd4  10365  elfzo1  10420  infssuzcldc  10485  expcllem  10802  expcl2lemap  10803  m1expcl2  10813  bcm1k  11012  bcpasc  11018  wrdv  11119  ccatclab  11161  pfxfv0  11263  pfxfvlsw  11266  cau3lem  11665  climconst2  11842  fsum3  11938  binomlem  12034  fprodge1  12190  cos12dec  12319  dvdsflip  12402  isprm3  12680  phimullem  12787  prmdiveq  12798  structcnvcnv  13088  fvsetsid  13106  ptex  13337  nmzsubg  13787  nmznsg  13790  nzrring  14187  lringnzr  14197  rege0subm  14588  znrrg  14664  tgval2  14765  qtopbasss  15235  dedekindicc  15347  ivthinc  15357  ivthdec  15358  dvply2  15481  cosz12  15494  cos0pilt1  15566  ioocosf1o  15568  mpodvdsmulf1o  15704  fsumdvdsmul  15705  lgsquadlemofi  15795  lgsquadlem1  15796  lgsquadlem2  15797  wlk1walkdom  16156  exmidsbthrlem  16562