Theorem sseli 2055

Description: Membership inference from subclass relationship.

Hypothesis

Ref	Expression
sseli.1	|- A (_ B

Assertion

Ref	Expression
sseli	|- (C e. A -> C e. B)

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 |- A (_ B
2		ssel 2053	. 2 |- (A (_ B -> (C e. A -> C e. B))
3	1, 2	ax-mp 7	1 |- (C e. A -> C e. B)

Syntax hints:   -> wi 3   e. wcel 955   (_ wss 2037

This theorem is referenced by:  sselii 2056  elun1 2187  elun2 2188  onfr 2976  nnont 3128  finds 3146  finds2 3148  brelg 3212  asymref 3423  asymref2 3424  2elresin 3584  fvopab4ndm 3769  fvimacnvi 3789  tz7.44-3 3915  eloprabi 4102  zfregs 4619  tz9.12lem3 4633  cplem1 4692  hta 4700  kmlem1 4737  zorn2lem3 4762  zorn2lem4 4763  zorn2lem5 4764  brdom5 4774  brdom4 4775  alephfplem3 4870  alephfp 4872  pinn 4978  recnt 5285  rexrt 5471  nnret 5877  nncnt 5878  nnind 5885  lbcl 5993  nnnn0t 6053  nn0ret 6055  nn0cnt 6056  nnzt 6100  nn0zt 6101  dfuz 6150  uzwo4OLD 6158  nnqt 6204  qcnt 6205  rpret 6222  om2uzlt 6235  om2uzlt2 6236  om2uzf1o 6238  uzssz 6362  expcllem 6507  cau3i 6851  cau5i 6854  cvg3 6860  clm3 7017  clm4 7018  clm4f 7020  climconst 7031  serzf0 7105  ser1f0 7106  ivthlem5 7220  dsupivthlem 7226  ivthlem5OLD 7229  efsep 7337  reeff1olem1 7364  reeff1olem1OLD 7366  unbenlem 7447  tgval2t 7559  cncnplem4 7716  caussi 7889  bcthlem14 7946  issubgi 8059  ghsubgi 8075  vcoprnelem 8135  vcex 8137  nvvcop 8151  nvvop 8166  phnv 8404  minveclem4 8479  minveclem5 8480  minveclem9 8484  minveclem10 8485  minveclem14 8489  minveclem16 8491  minveclem17 8492  minveclem28 8503  minveclem30 8505  minveclem31 8506  minveclem38 8513  minveceu 8514  pilem1 8590  pilem2 8591  efghgrpilem 8634  efifolem1 8637  relogeft 8685  relogeftb 8687  explogt 8694  shel 9003  chsh 9017  chel 9023  occl 9097  choc1 9206  shintcl 9208  chintcl 9210  shslej 9253  osumlem2 9496  osumlem4 9498  pjocin 9560  pjin 9561  mayete3 9590  dmadjopt 9737  nlelsh 9908  cnlnadjeu 9925  cnlnssadj 9928  bdopadjt 9930  hmopidmch 9990  hmopidmpj 9991  pjima 10015  atelch 10179  cdrci 10381  dmhmpha 10421  rnhmpha 10422  fgsb 10444  fgsb2 10449  iintlem2 10477

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain