# Metamath Proof Explorer

## Theorem dfiin2g

Description: Alternate definition of indexed intersection when B is a set. (Contributed by Jeff Hankins, 27-Aug-2009)

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

### Proof

Step Hyp Ref Expression
1 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {w}\in {B}\right)$
2 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {B}\in {C}\right)$
3 eleq2 ${⊢}{z}={B}\to \left({w}\in {z}↔{w}\in {B}\right)$
4 3 biimprcd ${⊢}{w}\in {B}\to \left({z}={B}\to {w}\in {z}\right)$
5 4 alrimiv ${⊢}{w}\in {B}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)$
6 eqid ${⊢}{B}={B}$
7 eqeq1 ${⊢}{z}={B}\to \left({z}={B}↔{B}={B}\right)$
8 7 3 imbi12d ${⊢}{z}={B}\to \left(\left({z}={B}\to {w}\in {z}\right)↔\left({B}={B}\to {w}\in {B}\right)\right)$
9 8 spcgv ${⊢}{B}\in {C}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\to \left({B}={B}\to {w}\in {B}\right)\right)$
10 6 9 mpii ${⊢}{B}\in {C}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\to {w}\in {B}\right)$
11 5 10 impbid2 ${⊢}{B}\in {C}\to \left({w}\in {B}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)$
12 11 imim2i ${⊢}\left({x}\in {A}\to {B}\in {C}\right)\to \left({x}\in {A}\to \left({w}\in {B}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)\right)$
13 12 pm5.74d ${⊢}\left({x}\in {A}\to {B}\in {C}\right)\to \left(\left({x}\in {A}\to {w}\in {B}\right)↔\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)\right)$
14 13 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {B}\in {C}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\to {w}\in {B}\right)↔\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)\right)$
15 albi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\to {w}\in {B}\right)↔\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {w}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)\right)$
16 14 15 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {B}\in {C}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {w}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)\right)$
17 2 16 sylbi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {C}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {w}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)\right)$
18 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({z}={B}\to {w}\in {z}\right)\right)$
19 18 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({z}={B}\to {w}\in {z}\right)\right)$
20 alcom ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({z}={B}\to {w}\in {z}\right)\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({z}={B}\to {w}\in {z}\right)\right)$
21 19 20 bitr4i ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({z}={B}\to {w}\in {z}\right)\right)$
22 r19.23v ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\to {w}\in {z}\right)$
23 vex ${⊢}{z}\in \mathrm{V}$
24 eqeq1 ${⊢}{y}={z}\to \left({y}={B}↔{z}={B}\right)$
25 24 rexbidv ${⊢}{y}={z}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right)$
26 23 25 elab ${⊢}{z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}$
27 26 imbi1i ${⊢}\left({z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\to {w}\in {z}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\to {w}\in {z}\right)$
28 22 27 bitr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)↔\left({z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\to {w}\in {z}\right)$
29 28 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\to {w}\in {z}\right)$
30 19.21v ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({z}={B}\to {w}\in {z}\right)\right)↔\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)$
31 30 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({z}={B}\to {w}\in {z}\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)$
32 21 29 31 3bitr3ri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={B}\to {w}\in {z}\right)\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\to {w}\in {z}\right)$
33 17 32 syl6bb ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {C}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {w}\in {B}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\to {w}\in {z}\right)\right)$
34 1 33 syl5bb ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {C}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in {B}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\to {w}\in {z}\right)\right)$
35 34 abbidv ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {C}\to \left\{{w}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in {B}\right\}=\left\{{w}|\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\to {w}\in {z}\right)\right\}$
36 df-iin ${⊢}\bigcap _{{x}\in {A}}{B}=\left\{{w}|\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in {B}\right\}$
37 df-int ${⊢}\bigcap \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}=\left\{{w}|\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\to {w}\in {z}\right)\right\}$
38 35 36 37 3eqtr4g ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {C}\to \bigcap _{{x}\in {A}}{B}=\bigcap \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}$