# Metamath Proof Explorer

## Theorem iinrab

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

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

### Proof

Step Hyp Ref Expression
1 r19.28zv ${⊢}{A}\ne \varnothing \to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {\phi }\right)↔\left({y}\in {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
2 1 abbidv ${⊢}{A}\ne \varnothing \to \left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {\phi }\right)\right\}=\left\{{y}|\left({y}\in {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right\}$
3 df-rab ${⊢}\left\{{y}\in {B}|{\phi }\right\}=\left\{{y}|\left({y}\in {B}\wedge {\phi }\right)\right\}$
4 3 a1i ${⊢}{x}\in {A}\to \left\{{y}\in {B}|{\phi }\right\}=\left\{{y}|\left({y}\in {B}\wedge {\phi }\right)\right\}$
5 4 iineq2i ${⊢}\bigcap _{{x}\in {A}}\left\{{y}\in {B}|{\phi }\right\}=\bigcap _{{x}\in {A}}\left\{{y}|\left({y}\in {B}\wedge {\phi }\right)\right\}$
6 iinab ${⊢}\bigcap _{{x}\in {A}}\left\{{y}|\left({y}\in {B}\wedge {\phi }\right)\right\}=\left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {\phi }\right)\right\}$
7 5 6 eqtri ${⊢}\bigcap _{{x}\in {A}}\left\{{y}\in {B}|{\phi }\right\}=\left\{{y}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {\phi }\right)\right\}$
8 df-rab ${⊢}\left\{{y}\in {B}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}=\left\{{y}|\left({y}\in {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right\}$
9 2 7 8 3eqtr4g ${⊢}{A}\ne \varnothing \to \bigcap _{{x}\in {A}}\left\{{y}\in {B}|{\phi }\right\}=\left\{{y}\in {B}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right\}$