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	⊢ ( ( ∪ 𝐴 ∩ 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		nne	⊢ ( ¬ ( 𝑥 ∩ 𝐵 ) ≠ ∅ ↔ ( 𝑥 ∩ 𝐵 ) = ∅ )
2	1	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ∩ 𝐵 ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) = ∅ )
3		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ∩ 𝐵 ) ≠ ∅ ↔ ¬ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) ≠ ∅ )
4		unissb	⊢ ( ∪ 𝐴 ⊆ ( V ∖ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ( V ∖ 𝐵 ) )
5		disj2	⊢ ( ( ∪ 𝐴 ∩ 𝐵 ) = ∅ ↔ ∪ 𝐴 ⊆ ( V ∖ 𝐵 ) )
6		disj2	⊢ ( ( 𝑥 ∩ 𝐵 ) = ∅ ↔ 𝑥 ⊆ ( V ∖ 𝐵 ) )
7	6	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ( V ∖ 𝐵 ) )
8	4 5 7	3bitr4ri	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) = ∅ ↔ ( ∪ 𝐴 ∩ 𝐵 ) = ∅ )
9	2 3 8	3bitr3i	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) ≠ ∅ ↔ ( ∪ 𝐴 ∩ 𝐵 ) = ∅ )
10	9	necon1abii	⊢ ( ( ∪ 𝐴 ∩ 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐵 ) ≠ ∅ )