Metamath Proof Explorer


Theorem rabfi

Description: A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017)

Ref Expression
Assertion rabfi ( 𝐴 ∈ Fin → { 𝑥𝐴𝜑 } ∈ Fin )

Proof

Step Hyp Ref Expression
1 dfrab3 { 𝑥𝐴𝜑 } = ( 𝐴 ∩ { 𝑥𝜑 } )
2 infi ( 𝐴 ∈ Fin → ( 𝐴 ∩ { 𝑥𝜑 } ) ∈ Fin )
3 1 2 eqeltrid ( 𝐴 ∈ Fin → { 𝑥𝐴𝜑 } ∈ Fin )