Theorem sseli 3234

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

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

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 3217  df-ss 3224

This theorem is referenced by:  sselii  3235  sselid  3236  elun1  3386  elun2  3387  elopabr  4401  elopabran  4402  finds  4722  finds2  4723  issref  5145  2elresin  5469  fvun1  5743  fvmptssdm  5762  elfvmptrab1  5772  fvimacnvi  5792  elpreima  5797  ofrfval  6275  ofvalg  6276  off  6279  offres  6328  eqopi  6366  op1steq  6373  dfoprab4  6386  f1od2  6431  reldmtpos  6484  smores3  6524  smores2  6525  ctssdccl  7402  pinn  7624  indpi  7657  enq0enq  7746  preqlu  7787  elinp  7789  prop  7790  elnp1st2nd  7791  prarloclem5  7815  cauappcvgprlemladd  7973  peano5nnnn  8207  nnindnn  8208  recn  8260  rexr  8319  peano5nni  9240  nnre  9244  nncn  9245  nnind  9253  nnnn0  9503  nn0re  9505  nn0cn  9506  nn0xnn0  9567  nnz  9596  nn0z  9597  uzuzle35  9897  nnq  9965  qcn  9966  rpre  9993  iccshftri  10328  iccshftli  10330  iccdili  10332  icccntri  10334  fzval2  10345  fzelp1  10408  4fvwrd4  10474  elfzo1  10530  infssuzcldc  10595  expcllem  10912  expcl2lemap  10913  m1expcl2  10923  bcm1k  11122  bcpasc  11128  hashfibclem  11206  wrdv  11240  ccatclab  11282  pfxfv0  11384  pfxfvlsw  11387  cau3lem  11799  climconst2  11976  fsum3  12073  binomlem  12169  fprodge1  12325  cos12dec  12454  dvdsflip  12537  isprm3  12815  phimullem  12922  prmdiveq  12933  structcnvcnv  13228  fvsetsid  13246  ptex  13477  nmzsubg  13927  nmznsg  13930  nzrring  14328  lringnzr  14338  rege0subm  14732  znrrg  14808  psrbagconf1o  14828  tgval2  14916  qtopbasss  15386  dedekindicc  15498  ivthinc  15508  ivthdec  15509  dvply2  15632  cosz12  15645  cos0pilt1  15717  ioocosf1o  15719  mpodvdsmulf1o  15858  fsumdvdsmul  15859  lgsquadlemofi  15949  lgsquadlem1  15950  lgsquadlem2  15951  wlk1walkdom  16354  exmidsbthrlem  16802