Theorem ssel 2615

Description: Membership relationships follow from a subclass relationship.

Assertion

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

Proof of Theorem ssel

Step	Hyp	Ref	Expression
1		dfss2 2610	. . . . . 6 |- (A C_ B <-> A.x(x e. A -> x e. B))
2	1	biimpi 168	. . . . 5 |- (A C_ B -> A.x(x e. A -> x e. B))
3	2	19.21bi 1408	. . . 4 |- (A C_ B -> (x e. A -> x e. B))
4	3	anim2d 620	. . 3 |- (A C_ B -> ((x = C /\ x e. A) -> (x = C /\ x e. B)))
5	4	eximdv 1669	. 2 |- (A C_ B -> (E.x(x = C /\ x e. A) -> E.x(x = C /\ x e. B)))
6		df-clel 1880	. 2 |- (C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 1880	. 2 |- (C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3imtr4g 612	1 |- (A C_ B -> (C e. A -> C e. B))

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   C_ wss 2593

This theorem is referenced by:  ssel2 2616  sseli 2617  sseld 2619  sstr2 2623  ssralv 2672  ssrexv 2673  ssconb 2738  sscon 2739  ssdif 2740  unss1 2773  ssrin 2817  reuss2 2870  reupick 2874  reldisjOLD 2917  prssOLD 3139  sssn 3142  tpssOLD 3146  uniss 3199  unissOLD 3200  iunss1OLD 3267  ss2iun 3271  ss2iunOLD 3272  ssiun 3293  ssiunOLD 3294  iinss 3304  sspwb 3503  unipw 3504  pwssun 3578  poss 3592  possOLD 3593  soss 3606  sossOLD 3607  onfr 3702  oneqmini 3714  sucssel 3763  onssneli 3779  onssnel2i 3780  snsn0nonOLD 3789  reuuniss 3815  mouniss 3816  reuuniss2 3817  elpwunsn 3856  ssorduni 3870  ssorduniOLD 3871  onint 3876  oninton 3881  ssnlim 3970  brrelex 4028  weinxp 4059  ssrel 4075  ssrelOLD 4076  ssrelrel 4083  ssrelrelOLD 4084  xpss12 4089  xpss12OLD 4090  cnvss 4134  dmss 4156  elreldm 4185  dmcosseq 4214  relssres 4248  iss 4254  issOLD 4255  resopab2 4256  cotrOLD 4303  cnvsymOLD 4305  ssrnres 4354  dfco2a 4394  cores 4400  coresOLD 4401  funssOLD 4440  funopg 4454  funssres 4460  fununi 4481  dfimafn 4720  funimass4 4722  fvelimabOLD 4726  funimass3 4779  dff3 4790  dff4 4791  rnssopab 4798  fopabcos 4806  funfvima2 4829  funfvima3 4830  isomin 4876  isofrlem 4878  reiotass2 5111  onfununi 5116  tfrlem1 5119  tfrlem13 5131  tz7.48lem 5164  tz7.49 5168  omsmolem 5313  omsmo 5314  ss2ixp 5413  onomeneq 5612  unblem1 5633  unblem3 5635  fiint 5650  inf3lem2 5720  r1tr 5765  tz9.13 5774  rankr1lem 5784  rankel 5791  rankval3 5792  bndrank 5793  rankpw 5795  cardlim 6003  carduni 6010  cfub 6056  suplem1pr 6313  supsr 6383  suprelem 6411  pre-axsup 6444  lbreu 7254  lbinfm 7257  sup2 7260  sup3 7261  infm3 7263  infmsup 7277  infmrcl 7278  xrsupsslem 7285  xrinfmsslem 7286  supxrre 7292  supxrpnf 7297  supxrunb1 7298  supxrunb2 7299  uzwo4OLD 7422  uzwo5OLD 7423  iccsupr 7567  uzwo 7624  uzwoOLD 7625  infxpidmlem7 8827  infmap2lem1 8848  tgval3 8895  basgen2 8909  subbas2 8915  ntrss2 8966  elcls2 8981  cncnplem3 9053  metreslem 9099  opnin 9146  cncfmet 9183  metelcls 9243  ssga 9455  ubthlem10 9881  flimopn 10321  cncomp 10331  ocsh 10789  occon 10793  ococss 10799  shorth 10801  shlessi 10980  spansnss2 11131  h1datomi 11137  pjss2i 11260  pjssmii 11261  pjorthcoi 11741  pj3si 11780  bnj1063 12899  bnj1171 13439  eqreznegel 13654  negn0 13655  gcdcllem1 13718  dfon2lem6 13854  wfrlem10 13966  nofv 13998  axdenselem3 14021  nocvxminlem 14028  nocvxmin 14029  axfelem14 14044  imgfldref2 14368  ref4w 14370  prj1 14395  inclrel 14444  eqfnung2 14459  inpreima2 14468  npincppr 14501  pospos 14635  rngsubpos 14636  intfmu2 14867  cnrsfin 14868  supexr 15043  cmpmorp 15126  dualalg 15131  idsubfun 15206  taralt 15211  emptar 15231  tarcrpr 15237  intartar 15255  vtarsuelt 15272  fnctartar 15284  fnctartar2 15285  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0 15436  alexsublem2 15438  alexsub 15441  reconn 15451  locfincomp 15514  locfincf 15516  comppfsc 15517  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  topmtcl 15525  topjoin 15527  fnejoin1 15530  fnejoin2 15531  filssufillem 15570  fcluscomplem 15620  fcluscomp 15621  difin2 15676  resoprab2 15710  f1elima 15719  fimax 15746  inficl 15757  fimaxre 15774  blssp 15844  totbndss 15937  ismtyres 15954  heiborlem13 15967  heiborlem23 15977  ispridlc 16218  sspwtr 16643  sspwtrALT 16644  sspwtrALT2 16645  pwtrVD 16646  pwtr 16647  pwtrrVD 16648  pwtrr 16649  suctrALT2VD 16660  suctrALT2 16661  lubel 16898  clatleglb 16903  paddss1 17278  paddss2 17279

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