Metamath Proof Explorer
Description: Membership inference from subclass relationship. (Contributed by NM, 31May1999)


Ref 
Expression 

Hypotheses 
sseli.1 
$${\u22a2}{A}\subseteq {B}$$ 


sselii.2 
$${\u22a2}{C}\in {A}$$ 

Assertion 
sselii 
$${\u22a2}{C}\in {B}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

sseli.1 
$${\u22a2}{A}\subseteq {B}$$ 
2 

sselii.2 
$${\u22a2}{C}\in {A}$$ 
3 
1

sseli 
$${\u22a2}{C}\in {A}\to {C}\in {B}$$ 
4 
2 3

axmp 
$${\u22a2}{C}\in {B}$$ 