Metamath Proof Explorer

Theorem abrexfi

Description: An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014)

Ref Expression
Assertion abrexfi ⊢ A ∈ Fin → y | ∃ x ∈ A y = B ∈ Fin

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
2 1 rnmpt ⊢ ran ⁡ x ∈ A ⟼ B = y | ∃ x ∈ A y = B
3 mptfi ⊢ A ∈ Fin → x ∈ A ⟼ B ∈ Fin
4 rnfi ⊢ x ∈ A ⟼ B ∈ Fin → ran ⁡ x ∈ A ⟼ B ∈ Fin
5 3 4 syl ⊢ A ∈ Fin → ran ⁡ x ∈ A ⟼ B ∈ Fin
6 2 5 eqeltrrid ⊢ A ∈ Fin → y | ∃ x ∈ A y = B ∈ Fin