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 A x = A
2 elsni y A y = A
3 1 2 ineqan12d x A y A x y = A A
4 inidm A A = A
5 3 4 syl6eq x A y A x y = A
6 vex x V
7 6 inex1 x y V
8 7 elsn x y A x y = A
9 5 8 sylibr x A y A x y A
10 9 rgen2 x A y A x y A
11 snex A V
12 inficl A V x A y A x y A fi A = A
13 11 12 ax-mp x A y A x y A fi A = A
14 10 13 mpbi fi A = A