Theorem sseli 3193

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

Syntax hints:   → wi 4   ∈ wcel 2177   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  sselii  3194  sselid  3195  elun1  3344  elun2  3345  finds  4656  finds2  4657  issref  5074  2elresin  5396  fvun1  5658  fvmptssdm  5677  elfvmptrab1  5687  fvimacnvi  5707  elpreima  5712  ofrfval  6180  ofvalg  6181  off  6184  offres  6233  eqopi  6271  op1steq  6278  dfoprab4  6291  f1od2  6334  reldmtpos  6352  smores3  6392  smores2  6393  ctssdccl  7228  pinn  7442  indpi  7475  enq0enq  7564  preqlu  7605  elinp  7607  prop  7608  elnp1st2nd  7609  prarloclem5  7633  cauappcvgprlemladd  7791  peano5nnnn  8025  nnindnn  8026  recn  8078  rexr  8138  peano5nni  9059  nnre  9063  nncn  9064  nnind  9072  nnnn0  9322  nn0re  9324  nn0cn  9325  nn0xnn0  9382  nnz  9411  nn0z  9412  nnq  9774  qcn  9775  rpre  9802  iccshftri  10137  iccshftli  10139  iccdili  10141  icccntri  10143  fzval2  10153  fzelp1  10216  4fvwrd4  10282  elfzo1  10336  infssuzcldc  10400  expcllem  10717  expcl2lemap  10718  m1expcl2  10728  bcm1k  10927  bcpasc  10933  wrdv  11032  ccatclab  11073  pfxfv0  11168  pfxfvlsw  11171  cau3lem  11500  climconst2  11677  fsum3  11773  binomlem  11869  fprodge1  12025  cos12dec  12154  dvdsflip  12237  isprm3  12515  phimullem  12622  prmdiveq  12633  structcnvcnv  12923  fvsetsid  12941  ptex  13171  nmzsubg  13621  nmznsg  13624  nzrring  14020  lringnzr  14030  rege0subm  14421  znrrg  14497  tgval2  14598  qtopbasss  15068  dedekindicc  15180  ivthinc  15190  ivthdec  15191  dvply2  15314  cosz12  15327  cos0pilt1  15399  ioocosf1o  15401  mpodvdsmulf1o  15537  fsumdvdsmul  15538  lgsquadlemofi  15628  lgsquadlem1  15629  lgsquadlem2  15630  exmidsbthrlem  16102