Theorem sseli 3233

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

Syntax hints:   → wi 4   ∈ wcel 2203   ⊆ wss 3210

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  sselii  3234  sselid  3235  elun1  3385  elun2  3386  elopabr  4400  elopabran  4401  finds  4721  finds2  4722  issref  5144  2elresin  5468  fvun1  5742  fvmptssdm  5761  elfvmptrab1  5771  fvimacnvi  5791  elpreima  5796  ofrfval  6274  ofvalg  6275  off  6278  offres  6327  eqopi  6365  op1steq  6372  dfoprab4  6385  f1od2  6430  reldmtpos  6483  smores3  6523  smores2  6524  ctssdccl  7401  pinn  7623  indpi  7656  enq0enq  7745  preqlu  7786  elinp  7788  prop  7789  elnp1st2nd  7790  prarloclem5  7814  cauappcvgprlemladd  7972  peano5nnnn  8206  nnindnn  8207  recn  8259  rexr  8318  peano5nni  9239  nnre  9243  nncn  9244  nnind  9252  nnnn0  9502  nn0re  9504  nn0cn  9505  nn0xnn0  9566  nnz  9595  nn0z  9596  uzuzle35  9896  nnq  9964  qcn  9965  rpre  9992  iccshftri  10327  iccshftli  10329  iccdili  10331  icccntri  10333  fzval2  10344  fzelp1  10407  4fvwrd4  10473  elfzo1  10529  infssuzcldc  10594  expcllem  10911  expcl2lemap  10912  m1expcl2  10922  bcm1k  11121  bcpasc  11127  hashfibclem  11202  wrdv  11236  ccatclab  11278  pfxfv0  11380  pfxfvlsw  11383  cau3lem  11795  climconst2  11972  fsum3  12069  binomlem  12165  fprodge1  12321  cos12dec  12450  dvdsflip  12533  isprm3  12811  phimullem  12918  prmdiveq  12929  structcnvcnv  13220  fvsetsid  13238  ptex  13469  nmzsubg  13919  nmznsg  13922  nzrring  14320  lringnzr  14330  rege0subm  14724  znrrg  14800  psrbagconf1o  14820  tgval2  14908  qtopbasss  15378  dedekindicc  15490  ivthinc  15500  ivthdec  15501  dvply2  15624  cosz12  15637  cos0pilt1  15709  ioocosf1o  15711  mpodvdsmulf1o  15850  fsumdvdsmul  15851  lgsquadlemofi  15941  lgsquadlem1  15942  lgsquadlem2  15943  wlk1walkdom  16346  exmidsbthrlem  16794