# Metamath Proof Explorer

## Theorem fisn

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

Ref Expression
Assertion fisn ${⊢}\mathrm{fi}\left(\left\{{A}\right\}\right)=\left\{{A}\right\}$

### Proof

Step Hyp Ref Expression
1 elsni ${⊢}{x}\in \left\{{A}\right\}\to {x}={A}$
2 elsni ${⊢}{y}\in \left\{{A}\right\}\to {y}={A}$
3 1 2 ineqan12d ${⊢}\left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\right)\to {x}\cap {y}={A}\cap {A}$
4 inidm ${⊢}{A}\cap {A}={A}$
5 3 4 syl6eq ${⊢}\left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\right)\to {x}\cap {y}={A}$
6 vex ${⊢}{x}\in \mathrm{V}$
7 6 inex1 ${⊢}{x}\cap {y}\in \mathrm{V}$
8 7 elsn ${⊢}{x}\cap {y}\in \left\{{A}\right\}↔{x}\cap {y}={A}$
9 5 8 sylibr ${⊢}\left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\right)\to {x}\cap {y}\in \left\{{A}\right\}$
10 9 rgen2 ${⊢}\forall {x}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \left\{{A}\right\}$
11 snex ${⊢}\left\{{A}\right\}\in \mathrm{V}$
12 inficl ${⊢}\left\{{A}\right\}\in \mathrm{V}\to \left(\forall {x}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \left\{{A}\right\}↔\mathrm{fi}\left(\left\{{A}\right\}\right)=\left\{{A}\right\}\right)$
13 11 12 ax-mp ${⊢}\forall {x}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{A}\right\}\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \left\{{A}\right\}↔\mathrm{fi}\left(\left\{{A}\right\}\right)=\left\{{A}\right\}$
14 10 13 mpbi ${⊢}\mathrm{fi}\left(\left\{{A}\right\}\right)=\left\{{A}\right\}$