Theorem unimax

Description: Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002)

	Ref	Expression
Assertion	unimax	$$⊢A\in B\to \bigcup \left\{x\in B|x\subseteq A\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢A\subseteq A$$
2		sseq1	$$⊢x=A\to \left(x\subseteq A\leftrightarrow A\subseteq A\right)$$
3	2	elrab3	$$⊢A\in B\to \left(A\in \left\{x\in B|x\subseteq A\right\}\leftrightarrow A\subseteq A\right)$$
4	1 3	mpbiri	$$⊢A\in B\to A\in \left\{x\in B|x\subseteq A\right\}$$
5		sseq1	$$⊢x=y\to \left(x\subseteq A\leftrightarrow y\subseteq A\right)$$
6	5	elrab	$$⊢y\in \left\{x\in B|x\subseteq A\right\}\leftrightarrow \left(y\in B\wedge y\subseteq A\right)$$
7	6	simprbi	$$⊢y\in \left\{x\in B|x\subseteq A\right\}\to y\subseteq A$$
8	7	rgen	$$⊢\forall y\in \left\{x\in B|x\subseteq A\right\}y\subseteq A$$
9		ssunieq	$$⊢\left(A\in \left\{x\in B|x\subseteq A\right\}\wedge \forall y\in \left\{x\in B|x\subseteq A\right\}y\subseteq A\right)\to A=\bigcup \left\{x\in B|x\subseteq A\right\}$$
10	9	eqcomd	$$⊢\left(A\in \left\{x\in B|x\subseteq A\right\}\wedge \forall y\in \left\{x\in B|x\subseteq A\right\}y\subseteq A\right)\to \bigcup \left\{x\in B|x\subseteq A\right\}=A$$
11	4 8 10	sylancl	$$⊢A\in B\to \bigcup \left\{x\in B|x\subseteq A\right\}=A$$