Metamath Proof Explorer


Theorem ssfii

Description: Any element of a set A is the intersection of a finite subset of A . (Contributed by FL, 27-Apr-2008) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion ssfii AVAfiA

Proof

Step Hyp Ref Expression
1 vex xV
2 1 intsn x=x
3 simpl AVxAAV
4 simpr AVxAxA
5 4 snssd AVxAxA
6 1 snnz x
7 6 a1i AVxAx
8 snfi xFin
9 8 a1i AVxAxFin
10 elfir AVxAxxFinxfiA
11 3 5 7 9 10 syl13anc AVxAxfiA
12 2 11 eqeltrrid AVxAxfiA
13 12 ex AVxAxfiA
14 13 ssrdv AVAfiA