# Metamath Proof Explorer

## Theorem iinab

Description: Indexed intersection of a class abstraction. (Contributed by NM, 6-Dec-2011)

Ref Expression
Assertion iinab ${⊢}\bigcap _{{x}\in {A}}\left\{{y}|{\phi }\right\}=\left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
2 nfab1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{{y}|{\phi }\right\}$
3 1 2 nfiin ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\bigcap _{{x}\in {A}}\left\{{y}|{\phi }\right\}$
4 nfab1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}$
5 3 4 cleqf ${⊢}\bigcap _{{x}\in {A}}\left\{{y}|{\phi }\right\}=\left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \bigcap _{{x}\in {A}}\left\{{y}|{\phi }\right\}↔{y}\in \left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}\right)$
6 abid ${⊢}{y}\in \left\{{y}|{\phi }\right\}↔{\phi }$
7 6 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left\{{y}|{\phi }\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
8 eliin ${⊢}{y}\in \mathrm{V}\to \left({y}\in \bigcap _{{x}\in {A}}\left\{{y}|{\phi }\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left\{{y}|{\phi }\right\}\right)$
9 8 elv ${⊢}{y}\in \bigcap _{{x}\in {A}}\left\{{y}|{\phi }\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left\{{y}|{\phi }\right\}$
10 abid ${⊢}{y}\in \left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
11 7 9 10 3bitr4i ${⊢}{y}\in \bigcap _{{x}\in {A}}\left\{{y}|{\phi }\right\}↔{y}\in \left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}$
12 5 11 mpgbir ${⊢}\bigcap _{{x}\in {A}}\left\{{y}|{\phi }\right\}=\left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}$