Theorem rintn0

Description: Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015) (Revised by Mario Carneiro, 5-Jun-2015)

	Ref	Expression
Assertion	rintn0	$$⊢\left(X\subseteq 𝒫A\wedge X\ne \varnothing \right)\to A\cap \bigcap X=\bigcap X$$

Proof

Step	Hyp	Ref	Expression
1		intssuni2	$$⊢\left(X\subseteq 𝒫A\wedge X\ne \varnothing \right)\to \bigcap X\subseteq \bigcup 𝒫A$$
2		ssid	$$⊢𝒫A\subseteq 𝒫A$$
3		sspwuni	$$⊢𝒫A\subseteq 𝒫A\leftrightarrow \bigcup 𝒫A\subseteq A$$
4	2 3	mpbi	$$⊢\bigcup 𝒫A\subseteq A$$
5	1 4	sstrdi	$$⊢\left(X\subseteq 𝒫A\wedge X\ne \varnothing \right)\to \bigcap X\subseteq A$$
6		sseqin2	$$⊢\bigcap X\subseteq A\leftrightarrow A\cap \bigcap X=\bigcap X$$
7	5 6	sylib	$$⊢\left(X\subseteq 𝒫A\wedge X\ne \varnothing \right)\to A\cap \bigcap X=\bigcap X$$