Theorem ssunib

Description: Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	ssunib	$$⊢A\subseteq \bigcup B\leftrightarrow \forall x\in A\exists y\in Bx\in y$$

Proof

Step	Hyp	Ref	Expression
1		dfss3	$$⊢A\subseteq \bigcup B\leftrightarrow \forall x\in Ax\in \bigcup B$$
2		eluni2	$$⊢x\in \bigcup B\leftrightarrow \exists y\in Bx\in y$$
3	2	ralbii	$$⊢\forall x\in Ax\in \bigcup B\leftrightarrow \forall x\in A\exists y\in Bx\in y$$
4	1 3	bitri	$$⊢A\subseteq \bigcup B\leftrightarrow \forall x\in A\exists y\in Bx\in y$$