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\in V\to \left|A\cap B\right|\le \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢A\cap B\subseteq A$$
2		hashss	$$⊢\left(A\in V\wedge A\cap B\subseteq A\right)\to \left|A\cap B\right|\le \left|A\right|$$
3	1 2	mpan2	$$⊢A\in V\to \left|A\cap B\right|\le \left|A\right|$$