Theorem sselii 2056

Description: Membership inference from subclass relationship.

Hypotheses

Ref	Expression
sseli.1	|- A (_ B
sselii.2	|- C e. A

Assertion

Ref	Expression
sselii	|- C e. B

Proof of Theorem sselii

Step	Hyp	Ref	Expression
1		sselii.2	. 2 |- C e. A
2		sseli.1	. . 3 |- A (_ B
3	2	sseli 2055	. 2 |- (C e. A -> C e. B)
4	1, 3	ax-mp 7	1 |- C e. B

Syntax hints:   e. wcel 955   (_ wss 2037

This theorem is referenced by:  tz7.44-1 3913  tz7.44-2 3914  alephfp2 4873  ax1cn 5241  recn 5286  nn0re 6057  cvg3 6860  clm4 7018  ivthlem9 7224  isupivth 7225  dsupivthlem 7226  ivth2OLD 7234  minvecle 8517  sheli 9004  cheli 9024  omlsilem 9159  nonbool 9513  pjssm 9543  riesz4t 9912  riesz1t 9913  cnlnadjeut 9926  nmopadjle 9936

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