Theorem sseli 2117

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 2115	. 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 994   (_ wss 2099

This theorem is referenced by:  sselii 2118  elun1 2249  elun2 2250  onfr 3014  nnon 3225  finds 3244  finds2 3246  brelg 3307  asymref 3531  asymref2 3532  2elresin 3704  fvopab4ndm 3895  fvimacnvi 3918  dfoprab4s 4176  eloprabi 4180  tz7.44-3 4231  zfregs 4793  tz9.12lem3 4807  cplem1 4866  hta 4874  kmlem1 4911  zorn2lem3 4936  zorn2lem4 4937  zorn2lem5 4938  brdom5 4948  brdom4 4949  alephfplem3 5048  alephfp 5050  pinn 5160  recn 5467  rexr 5653  nnre 6074  nncn 6075  nnind 6082  rpre 6195  lbcl 6214  nnnn0 6274  nn0re 6276  nn0cn 6277  nnz 6321  nn0z 6322  dfuzi 6373  uzwo4OLD 6381  nnq 6405  qcn 6406  uzssz 6557  om2uzlti 6661  om2uzlt2i 6662  om2uzf1oi 6664  expcllem 6770  cau3ii 7117  cau5ii 7120  cvg3i 7126  clm3i 7282  clm4i 7283  clm4fi 7285  climconsti 7297  serzf0i 7372  ivthlem5 7490  dsupivthlem 7496  efsepi 7604  unbenlem 7716  tgval2 7829  cncnplem4 7987  caussi 8165  bcthlem14 8223  issubgi 8364  ghsubgi 8379  vcoprnelem 8444  vcex 8446  nvvcop 8460  nvvop 8475  phnv 8729  minveclem4 8808  minveclem5 8809  minveclem9 8813  minveclem10 8814  minveclem14 8818  minveclem16 8820  minveclem17 8821  minveclem28 8832  minveclem30 8834  minveclem31 8835  minveclem38 8842  minveceu 8843  pilem1 8938  pilem2 8939  efghgrpilem 8991  efifolem1 8994  relogef 9035  relogeftb 9037  explog 9044  sheli 9358  chsh 9372  cheli 9378  occli 9457  choc1 9567  shintcli 9569  chintcli 9571  shsleji 9614  osumlem2 9857  osumlem4 9859  pjocini 9921  pjini 9922  mayete3i 9951  mayete3OLDi 9952  dmadjop 10100  nlelshi 10272  cnlnadjeui 10289  cnlnssadj 10292  bdopadj 10294  hmopidmchi 10359  hmopidmpji 10360  pjimai 10384  atelch 10552  nnssi2 10704  nnssi3 10705  domintref 10767  ref3w 10772  fldleqt 10795  inposet 10868  tostos 10883  opidon 10898  on1el3 10962  cdrci 10994  dmhmpha 11040  rnhmpha 11041  fgsb 11082  fgsb2 11086  fintopcomp 11115  bwt2 11123  empcon 11135  iintlem2 11156  besubbeca 11302  ordtypelem3 11429  ordtypelem4 11430  ordtypelem7 11433  subtopmetlem 11505  reconnlem3 11509  reconnlem4 11510  reconnlem5 11511  reconn 11512  ivthALT 11515  locfincomp 11575  comppfsc 11578  neibastop1 11579  filcon 11665  ufcondr 11666  filnetlem3 11765  elpreima 11792  difxp 11798  upxp 11822  sdclem1 11875  fsumltisumii 11885  fsumleisumii 11888  metsstop 11909  iccshftri 11923  iccshftli 11925  iccdili 11927  icccntri 11929  lincmb01cmp 11942  lincmb01icc 11943  tx1cn 11976  tx2cn 11977  totbndss 11993  heiborlem16 12026  heiborlem17 12027  heiborlem30 12040  heiborlem32 12042  heiborlem35 12045  heiborlem37 12047  rrntotbnd 12078  phtpycolem1 12093  phtpycolem2 12094

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain