Theorem sseli 2617

Description: Membership inference from subclass relationship.

Hypothesis

Ref	Expression
sseli.1	|- A C_ B

Assertion

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

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 |- A C_ B
2		ssel 2615	. 2 |- (A C_ 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 1300   C_ wss 2593

This theorem is referenced by:  sselii 2618  elun1 2771  elun2 2772  onfr 3702  nnon 3957  finds 3979  finds2 3981  brelg 4047  asymrefOLD 4309  asymref2OLD 4311  2elresin 4524  fvopab4ndm 4747  fvimacnvi 4777  dfoprab4s 5056  eloprabi 5060  tz7.44-3 5138  ordtypelem3 5686  ordtypelem4 5687  ordtypelem7 5690  zfregs 5754  tz9.12lem3 5772  cplem1 5850  hta 5858  kmlem1 5927  zorn2lem3 5952  zorn2lem4 5953  zorn2lem5 5954  brdom5 5964  brdom4 5965  alephfplem3 6046  alephfp 6048  pinn 6158  recn 6466  rexr 6668  nnre 7112  nncn 7113  nnind 7120  rpre 7236  lbcl 7255  nnnn0 7315  nn0re 7317  nn0cn 7318  nnz 7362  nn0z 7363  dfuzi 7414  uzwo4OLD 7422  nnq 7446  qcn 7447  uzssz 7599  om2uzlti 7709  om2uzlt2i 7710  om2uzf1oi 7712  expcllem 7818  cau3ii 8166  cau5ii 8169  cvg3i 8175  clm3i 8339  clm4i 8340  clm4fi 8342  climconsti 8354  serzf0i 8429  ivthlem5 8547  dsupivthlem 8553  efsepi 8661  unbenlem 8773  tgval2 8887  cncnplem4 9054  caussi 9232  bcthlem14 9290  issubgi 9431  ghsubgi 9446  vcoprnelem 9529  vcex 9531  nvvcop 9545  nvvop 9560  phnv 9814  minveclem4 9893  minveclem5 9894  minveclem9 9898  minveclem10 9899  minveclem14 9903  minveclem16 9905  minveclem17 9906  minveclem28 9917  minveclem30 9919  minveclem31 9920  minveclem38 9927  minveceu 9928  pilem1 10020  pilem2 10021  efghgrpilem 10073  efifolem1 10076  relogef 10117  relogeftb 10119  explog 10126  elpreima 10161  cdrci 10182  tx1cn 10223  tx2cn 10224  upxp 10225  subtopmetlem 10255  fintopcomp 10333  opidon 10369  on1el3 10412  sheli 10715  chsh 10729  cheli 10735  occli 10814  choc1 10924  shintcli 10926  chintcli 10928  shsleji 10971  osumlem2 11214  osumlem4 11216  pjocini 11278  pjini 11279  mayete3i 11308  mayete3OLDi 11309  dmadjop 11457  nlelshi 11630  cnlnadjeui 11647  cnlnssadj 11650  bdopadj 11652  hmopidmchi 11723  hmopidmpji 11724  pjimai 11748  atelch 11916  bnj46 12416  bnj49 12421  bnj1533 13182  bnj1137 13433  bnj1286 13481  bnj1404 13517  bnj1387 13526  ublbneg 13653  divalglem8 13703  isprm3 13776  dfon2lem4 13852  wfrlem4 13960  wfrlem10 13966  axfelem10 14040  nnssi2 14256  nnssi3 14257  ref4w 14370  inpreima5 14469  dstr 14516  posispre 14582  inposet 14620  istoset2 14628  tostos 14637  dffprod 14670  reacomsmgrp1 14703  reacomsmgrp2 14704  reacomsmgrp3 14705  reacomsmgrp4 14706  clfsebsr 14709  clfsebs2 14710  resgcom 14712  fprodadd 14713  dmhmpha 14888  rnhmpha 14889  stoig2b 14906  fgsb 14921  fgsb2 14925  bwt2 14960  empcon 14966  iintlem2 15011  fldleqt 15023  besubbeca 15196  inttaror 15277  ordtypelem3OLD 15377  ordtypelem4OLD 15378  ordtypelem7OLD 15381  reconnlem3 15448  reconnlem4 15449  reconnlem5 15450  reconn 15451  ivthALT 15454  locfincomp 15514  comppfsc 15517  neibastop1 15518  filcon 15580  ufcondr 15581  filnetlem3 15642  cover2 15673  opelopab3 15688  difxp 15690  sdclem1 15809  fsumltisumii 15822  fsumleisumii 15825  iccshftri 15858  iccshftli 15860  iccdili 15862  icccntri 15864  lincmb01cmp 15878  lincmb01icc 15879  oprpiece1res1 15880  oprpiece1res2 15881  cnresoprab 15915  totbndss 15937  heiborlem16 15970  heiborlem17 15971  heiborlem30 15984  heiborlem32 15986  heiborlem35 15989  heiborlem37 15991  rrntotbnd 16022  exidcl 16029  phtpycolem1 16051  phtpycolem2 16052  reparphtlem2 16064  reparpht 16065  pcoval2 16075  pcohtpylem1 16080  pcohtpylem2 16081  pcoass 16085  pcorevlem 16086  pcorev 16087  flddivrng 16113  smores2 16447  stbcl 16730  osumcllem7 17370  pexmidlem4 17381

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain