Theorem hashrabrex

Description: The number of elements in a class abstraction with a restricted existential quantification. (Contributed by Alexander van der Vekens, 29-Jul-2018)

	Ref	Expression
Hypotheses	hashrabrex.1	$$⊢\phi \to Y\in \mathrm{Fin}$$
	hashrabrex.2	$$⊢\left(\phi \wedge y\in Y\right)\to \left\{x\in X|\psi \right\}\in \mathrm{Fin}$$
	hashrabrex.3	$$⊢\phi \to \underset{y\in Y}{Disj}\left\{x\in X|\psi \right\}$$
Assertion	hashrabrex	$$⊢\phi \to \left|\left\{x\in X|\exists y\in Y\psi \right\}\right|=\sum _{y\in Y}\left|\left\{x\in X|\psi \right\}\right|$$

Proof

Step	Hyp	Ref	Expression
1		hashrabrex.1	$$⊢\phi \to Y\in \mathrm{Fin}$$
2		hashrabrex.2	$$⊢\left(\phi \wedge y\in Y\right)\to \left\{x\in X|\psi \right\}\in \mathrm{Fin}$$
3		hashrabrex.3	$$⊢\phi \to \underset{y\in Y}{Disj}\left\{x\in X|\psi \right\}$$
4		iunrab	$$⊢\bigcup _{y\in Y}\left\{x\in X|\psi \right\}=\left\{x\in X|\exists y\in Y\psi \right\}$$
5	4	eqcomi	$$⊢\left\{x\in X|\exists y\in Y\psi \right\}=\bigcup _{y\in Y}\left\{x\in X|\psi \right\}$$
6	5	fveq2i	$$⊢\left|\left\{x\in X|\exists y\in Y\psi \right\}\right|=\left|\bigcup _{y\in Y}\left\{x\in X|\psi \right\}\right|$$
7	1 2 3	hashiun	$$⊢\phi \to \left|\bigcup _{y\in Y}\left\{x\in X|\psi \right\}\right|=\sum _{y\in Y}\left|\left\{x\in X|\psi \right\}\right|$$
8	6 7	syl5eq	$$⊢\phi \to \left|\left\{x\in X|\exists y\in Y\psi \right\}\right|=\sum _{y\in Y}\left|\left\{x\in X|\psi \right\}\right|$$