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	|- ( ph -> Y e. Fin )
	hashrabrex.2	|- ( ( ph /\ y e. Y ) -> { x e. X | ps } e. Fin )
	hashrabrex.3	|- ( ph -> Disj_ y e. Y { x e. X | ps } )
Assertion	hashrabrex	|- ( ph -> ( # ` { x e. X | E. y e. Y ps } ) = sum_ y e. Y ( # ` { x e. X | ps } ) )

Proof

Step	Hyp	Ref	Expression
1		hashrabrex.1	|- ( ph -> Y e. Fin )
2		hashrabrex.2	|- ( ( ph /\ y e. Y ) -> { x e. X | ps } e. Fin )
3		hashrabrex.3	|- ( ph -> Disj_ y e. Y { x e. X | ps } )
4		iunrab	|- U_ y e. Y { x e. X | ps } = { x e. X | E. y e. Y ps }
5	4	eqcomi	|- { x e. X | E. y e. Y ps } = U_ y e. Y { x e. X | ps }
6	5	fveq2i	|- ( # ` { x e. X | E. y e. Y ps } ) = ( # ` U_ y e. Y { x e. X | ps } )
7	1 2 3	hashiun	|- ( ph -> ( # ` U_ y e. Y { x e. X | ps } ) = sum_ y e. Y ( # ` { x e. X | ps } ) )
8	6 7	eqtrid	|- ( ph -> ( # ` { x e. X | E. y e. Y ps } ) = sum_ y e. Y ( # ` { x e. X | ps } ) )