Theorem uniinn0

Description: Sufficient and necessary condition for a union to intersect with a given set. (Contributed by Thierry Arnoux, 27-Jan-2020)

	Ref	Expression
Assertion	uniinn0	$$⊢\bigcup A\cap B\ne \varnothing \leftrightarrow \exists x\in Ax\cap B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nne	$$⊢\neg x\cap B\ne \varnothing \leftrightarrow x\cap B=\varnothing$$
2	1	ralbii	$$⊢\forall x\in A\neg x\cap B\ne \varnothing \leftrightarrow \forall x\in Ax\cap B=\varnothing$$
3		ralnex	$$⊢\forall x\in A\neg x\cap B\ne \varnothing \leftrightarrow \neg \exists x\in Ax\cap B\ne \varnothing$$
4		unissb	$$⊢\bigcup A\subseteq \mathrm{V}\setminus B\leftrightarrow \forall x\in Ax\subseteq \mathrm{V}\setminus B$$
5		disj2	$$⊢\bigcup A\cap B=\varnothing \leftrightarrow \bigcup A\subseteq \mathrm{V}\setminus B$$
6		disj2	$$⊢x\cap B=\varnothing \leftrightarrow x\subseteq \mathrm{V}\setminus B$$
7	6	ralbii	$$⊢\forall x\in Ax\cap B=\varnothing \leftrightarrow \forall x\in Ax\subseteq \mathrm{V}\setminus B$$
8	4 5 7	3bitr4ri	$$⊢\forall x\in Ax\cap B=\varnothing \leftrightarrow \bigcup A\cap B=\varnothing$$
9	2 3 8	3bitr3i	$$⊢\neg \exists x\in Ax\cap B\ne \varnothing \leftrightarrow \bigcup A\cap B=\varnothing$$
10	9	necon1abii	$$⊢\bigcup A\cap B\ne \varnothing \leftrightarrow \exists x\in Ax\cap B\ne \varnothing$$