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 
|- ( A e. Fin -> { x e. A | ph } e. Fin )

Proof

Step Hyp Ref Expression
1 dfrab3 
 |-  { x e. A | ph } = ( A i^i { x | ph } )
2 infi 
 |-  ( A e. Fin -> ( A i^i { x | ph } ) e. Fin )
3 1 2 eqeltrid 
 |-  ( A e. Fin -> { x e. A | ph } e. Fin )