Theorem ssel 2053

Description: Membership relationships follow from a subclass relationship.

Assertion

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

Proof of Theorem ssel

Step	Hyp	Ref	Expression
1		dfss2 2048	. . . . . 6 |- (A (_ B <-> A.x(x e. A -> x e. B))
2	1	biimp 151	. . . . 5 |- (A (_ B -> A.x(x e. A -> x e. B))
3	2	19.21bi 1056	. . . 4 |- (A (_ B -> (x e. A -> x e. B))
4	3	anim2d 559	. . 3 |- (A (_ B -> ((x = C /\ x e. A) -> (x = C /\ x e. B)))
5	4	19.22dv 1285	. 2 |- (A (_ B -> (E.x(x = C /\ x e. A) -> E.x(x = C /\ x e. B)))
6		df-clel 1465	. 2 |- (C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 1465	. 2 |- (C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3imtr4g 551	1 |- (A (_ B -> (C e. A -> C e. B))

Syntax hints:   -> wi 3   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  E.wex 977   (_ wss 2037

This theorem is referenced by:  ssel2 2054  sseli 2055  sseld 2057  ssralv 2104  ssrexv 2105  ssconb 2160  sscon 2161  ssdif 2162  reuss2 2265  reupick 2269  reldisj 2303  prss 2462  sssn 2464  tpss 2467  uniss 2511  iunss1 2564  ss2iun 2567  ssiun 2582  sspwb 2745  unipw 2746  pwssun 2816  poss 2832  soss 2843  reuuniss 2879  mouniss 2880  reuuniss2 2881  elpwunsn 2902  onfr 2976  ssorduni 2983  onint 2996  oninton 3002  oneqmini 3007  sucssel 3060  onssneli 3091  onssneli2 3092  snsn0non 3115  ssnlim 3157  brrelex 3197  weinxp 3223  ssrel 3237  ssxp 3246  cnvss 3280  dmss 3299  elreldm 3327  relssres 3376  iss 3381  resopab2 3382  cotr 3420  cnvsym 3421  ssrnres 3467  cores 3485  funss 3520  funopg 3533  funssres 3538  fununi 3549  dfimafn 3746  funimass4 3748  fvelimab 3750  funimass3 3791  dff2 3802  dff3 3803  rnssopab 3810  fopabcos 3818  funfvima2 3838  funfvima3 3839  isomin 3884  isofrlem 3886  tfrlem1 3896  tfrlem13 3908  tz7.48lem 3940  tz7.49 3944  omsmolem 4240  omsmo 4241  ss2ixp 4338  onomeneq 4498  unblem1 4517  unblem3 4519  fiint 4534  inf3lem2 4586  r1tr 4626  tz9.13 4635  rankr1lem 4645  rankel 4652  rankval3 4653  bndrank 4654  rankpw 4656  cardlim 4823  carduni 4830  cfub 4880  suplem1pr 5133  supsr 5203  suprelem 5231  pre-axsup 5263  lbreu 5992  lbinfm 5995  sup2 5998  sup3 5999  infm3 6001  infmsup 6015  infmrcl 6016  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  supxrpnf 6035  supxrunb1 6036  supxrunb2 6037  uzwo4OLD 6158  uzwo5OLD 6159  iccsupr 6331  uzwo 6387  uzwoOLD 6388  infxpidmlem7 7501  infmap2lem1 7521  tgval3t 7567  basgen2t 7581  subbas2 7587  ntrss2 7632  elcls2 7647  cncnplem3 7715  metreslem 7762  opnin 7809  cncfmet 7844  metelcls 7900  ubthlem10 8469  ocsh 9072  occont 9076  ococss 9082  shorth 9084  shless 9262  spansnss2t 9415  h1datom 9421  pjss2 9542  pjssm 9543  pjorthco 10008  pj3s 10045  cnrsfin 10396  cmpmorp 10556

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain