Theorem sseli 2065

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 2063	. 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 958   (_ wss 2047

This theorem is referenced by:  sselii 2066  elun1 2197  elun2 2198  onfr 2986  nnont 3138  finds 3156  finds2 3158  brelg 3222  asymref 3439  asymref2 3440  2elresin 3598  fvopab4ndm 3784  fvimacnvi 3804  tz7.44-3 3930  eloprabi 4118  zfregs 4647  tz9.12lem3 4661  cplem1 4720  hta 4728  kmlem1 4765  zorn2lem3 4790  zorn2lem4 4791  zorn2lem5 4792  brdom5 4802  brdom4 4803  alephfplem3 4898  alephfp 4900  pinn 5006  recnt 5313  rexrt 5499  nnret 5929  nncnt 5930  nnind 5937  lbcl 6046  nnnn0t 6106  nn0ret 6108  nn0cnt 6109  nnzt 6153  nn0zt 6154  dfuz 6202  uzwo4OLD 6210  nnqt 6266  qcnt 6267  rpret 6284  om2uzlt 6298  om2uzlt2 6299  om2uzf1o 6301  uzssz 6430  expcllem 6575  cau3i 6914  cau5i 6917  cvg3 6923  clm3 7079  clm4 7080  clm4f 7082  climconst 7094  serzf0 7169  ser1f0 7170  ivthlem5 7285  dsupivthlem 7291  efsep 7396  unbenlem 7504  tgval2t 7617  cncnplem4 7777  caussi 7954  bcthlem14 8012  issubgi 8122  ghsubgi 8138  vcoprnelem 8197  vcex 8199  nvvcop 8213  nvvop 8228  phnv 8473  minveclem4 8548  minveclem5 8549  minveclem9 8553  minveclem10 8554  minveclem14 8558  minveclem16 8560  minveclem17 8561  minveclem28 8572  minveclem30 8574  minveclem31 8575  minveclem38 8582  minveceu 8583  pilem1 8671  pilem2 8672  efghgrpilem 8719  efifolem1 8722  relogeft 8763  relogeftb 8765  explogt 8772  shel 9082  chsh 9096  chel 9102  occl 9181  choc1 9291  shintcl 9293  chintcl 9295  shslej 9338  osumlem2 9579  osumlem4 9581  pjocin 9643  pjin 9644  mayete3 9673  dmadjopt 9820  nlelsh 9993  cnlnadjeu 10010  cnlnssadj 10013  bdopadjt 10015  hmopidmch 10079  hmopidmpj 10080  pjima 10104  atelch 10271  nnssi2 10419  nnssi3 10420  cdrci 10494  dmhmpha 10534  rnhmpha 10535  fgsb 10570  fgsbOLD 10571  fgsb2 10580  iintlem2 10633

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain