Theorem sseli 2062

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 2060	. 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 957   (_ wss 2044

This theorem is referenced by:  sselii 2063  elun1 2194  elun2 2195  onfr 2982  nnont 3134  finds 3152  finds2 3154  brelg 3218  asymref 3435  asymref2 3436  2elresin 3594  fvopab4ndm 3779  fvimacnvi 3799  tz7.44-3 3925  eloprabi 4111  zfregs 4630  tz9.12lem3 4644  cplem1 4703  hta 4711  kmlem1 4748  zorn2lem3 4773  zorn2lem4 4774  zorn2lem5 4775  brdom5 4785  brdom4 4786  alephfplem3 4881  alephfp 4883  pinn 4989  recnt 5296  rexrt 5482  nnret 5887  nncnt 5888  nnind 5895  lbcl 6003  nnnn0t 6063  nn0ret 6065  nn0cnt 6066  nnzt 6110  nn0zt 6111  dfuz 6160  uzwo4OLD 6168  nnqt 6216  qcnt 6217  rpret 6234  om2uzlt 6248  om2uzlt2 6249  om2uzf1o 6251  uzssz 6375  expcllem 6520  cau3i 6866  cau5i 6869  cvg3 6875  clm3 7032  clm4 7033  clm4f 7035  climconst 7047  serzf0 7122  ser1f0 7123  ivthlem5 7237  dsupivthlem 7243  ivthlem5OLD 7246  efsep 7354  reeff1olem1 7381  reeff1olem1OLD 7383  unbenlem 7464  tgval2t 7577  cncnplem4 7737  caussi 7916  bcthlem14 7974  issubgi 8086  ghsubgi 8102  vcoprnelem 8161  vcex 8163  nvvcop 8177  nvvop 8192  phnv 8432  minveclem4 8507  minveclem5 8508  minveclem9 8512  minveclem10 8513  minveclem14 8517  minveclem16 8519  minveclem17 8520  minveclem28 8531  minveclem30 8533  minveclem31 8534  minveclem38 8541  minveceu 8542  pilem1 8625  pilem2 8626  efghgrpilem 8669  efifolem1 8672  relogeft 8718  relogeftb 8720  explogt 8727  shel 9037  chsh 9051  chel 9057  occl 9136  choc1 9246  shintcl 9248  chintcl 9250  shslej 9293  osumlem2 9536  osumlem4 9538  pjocin 9600  pjin 9601  mayete3 9630  dmadjopt 9777  nlelsh 9949  cnlnadjeu 9966  cnlnssadj 9969  bdopadjt 9971  hmopidmch 10035  hmopidmpj 10036  pjima 10060  atelch 10227  nnssi2 10377  nnssi3 10378  cdrci 10440  dmhmpha 10480  rnhmpha 10481  fgsb 10503  fgsb2 10508  iintlem2 10549

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-in 2048  df-ss 2050

Copyright terms: Public domain