Metamath Proof Explorer

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	$⊢ φ \to B \in Fin$
		rabrexfi.2	$⊢ (φ \land y \in B) \to \{x \in A \| ψ\} \in Fin$
	Assertion	rabrexfi	$⊢ φ \to \{x \in A \| \exists y \in B ψ\} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		rabrexfi.1	$⊢ φ \to B \in Fin$
2		rabrexfi.2	$⊢ (φ \land y \in B) \to \{x \in A \| ψ\} \in Fin$
3		iunrab	$⊢ ⋃_{y \in B} \{x \in A \| ψ\} = \{x \in A \| \exists y \in B ψ\}$
4	2	ralrimiva	$⊢ φ \to \forall y \in B \{x \in A \| ψ\} \in Fin$
5		iunfi	$⊢ (B \in Fin \land \forall y \in B \{x \in A \| ψ\} \in Fin) \to ⋃_{y \in B} \{x \in A \| ψ\} \in Fin$
6	1 4 5	syl2anc	$⊢ φ \to ⋃_{y \in B} \{x \in A \| ψ\} \in Fin$
7	3 6	eqeltrrid	$⊢ φ \to \{x \in A \| \exists y \in B ψ\} \in Fin$