Theorem rabrexfi

Description: Conditions for a class abstraction with a restricted existential quantification to be finite. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	rabrexfi.1	|- ( ph -> B e. Fin )
	rabrexfi.2	|- ( ( ph /\ y e. B ) -> { x e. A | ps } e. Fin )
Assertion	rabrexfi	|- ( ph -> { x e. A | E. y e. B ps } e. Fin )

Proof

Step	Hyp	Ref	Expression
1		rabrexfi.1	|- ( ph -> B e. Fin )
2		rabrexfi.2	|- ( ( ph /\ y e. B ) -> { x e. A | ps } e. Fin )
3		iunrab	|- U_ y e. B { x e. A | ps } = { x e. A | E. y e. B ps }
4	2	ralrimiva	|- ( ph -> A. y e. B { x e. A | ps } e. Fin )
5		iunfi	|- ( ( B e. Fin /\ A. y e. B { x e. A | ps } e. Fin ) -> U_ y e. B { x e. A | ps } e. Fin )
6	1 4 5	syl2anc	|- ( ph -> U_ y e. B { x e. A | ps } e. Fin )
7	3 6	eqeltrrid	|- ( ph -> { x e. A | E. y e. B ps } e. Fin )