Metamath Proof Explorer

Theorem fisn

Description: A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion fisn 
|- ( fi ` { A } ) = { A }

Proof

Step Hyp Ref Expression
1 elsni 
 |-  ( x e. { A } -> x = A )
2 elsni 
 |-  ( y e. { A } -> y = A )
3 1 2 ineqan12d 
 |-  ( ( x e. { A } /\ y e. { A } ) -> ( x i^i y ) = ( A i^i A ) )
4 inidm 
 |-  ( A i^i A ) = A
5 3 4 eqtrdi 
 |-  ( ( x e. { A } /\ y e. { A } ) -> ( x i^i y ) = A )
6 vex 
 |-  x e. _V
7 6 inex1 
 |-  ( x i^i y ) e. _V
8 7 elsn 
 |-  ( ( x i^i y ) e. { A } <-> ( x i^i y ) = A )
9 5 8 sylibr 
 |-  ( ( x e. { A } /\ y e. { A } ) -> ( x i^i y ) e. { A } )
10 9 rgen2 
 |-  A. x e. { A } A. y e. { A } ( x i^i y ) e. { A }
11 snex 
 |-  { A } e. _V
12 inficl 
 |-  ( { A } e. _V -> ( A. x e. { A } A. y e. { A } ( x i^i y ) e. { A } <-> ( fi ` { A } ) = { A } ) )
13 11 12 ax-mp 
 |-  ( A. x e. { A } A. y e. { A } ( x i^i y ) e. { A } <-> ( fi ` { A } ) = { A } )
14 10 13 mpbi 
 |-  ( fi ` { A } ) = { A }