Metamath Proof Explorer

Theorem hashin

Description: The size of the intersection of a set and a class is less than or equal to the size of the set. (Contributed by AV, 4-Jan-2021)

Ref Expression
Assertion hashin 
|- ( A e. V -> ( # ` ( A i^i B ) ) <_ ( # ` A ) )

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( A i^i B ) C_ A
2 hashss 
 |-  ( ( A e. V /\ ( A i^i B ) C_ A ) -> ( # ` ( A i^i B ) ) <_ ( # ` A ) )
3 1 2 mpan2 
 |-  ( A e. V -> ( # ` ( A i^i B ) ) <_ ( # ` A ) )