# Metamath Proof Explorer

## Theorem intpr

Description: The intersection of a pair is the intersection of its members. Theorem 71 of Suppes p. 42. (Contributed by NM, 14-Oct-1999)

Ref Expression
Hypotheses intpr.1 ${⊢}{A}\in \mathrm{V}$
intpr.2 ${⊢}{B}\in \mathrm{V}$
Assertion intpr ${⊢}\bigcap \left\{{A},{B}\right\}={A}\cap {B}$

### Proof

Step Hyp Ref Expression
1 intpr.1 ${⊢}{A}\in \mathrm{V}$
2 intpr.2 ${⊢}{B}\in \mathrm{V}$
3 19.26 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}={A}\to {x}\in {y}\right)\wedge \left({y}={B}\to {x}\in {y}\right)\right)↔\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\to {x}\in {y}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={B}\to {x}\in {y}\right)\right)$
4 vex ${⊢}{y}\in \mathrm{V}$
5 4 elpr ${⊢}{y}\in \left\{{A},{B}\right\}↔\left({y}={A}\vee {y}={B}\right)$
6 5 imbi1i ${⊢}\left({y}\in \left\{{A},{B}\right\}\to {x}\in {y}\right)↔\left(\left({y}={A}\vee {y}={B}\right)\to {x}\in {y}\right)$
7 jaob ${⊢}\left(\left({y}={A}\vee {y}={B}\right)\to {x}\in {y}\right)↔\left(\left({y}={A}\to {x}\in {y}\right)\wedge \left({y}={B}\to {x}\in {y}\right)\right)$
8 6 7 bitri ${⊢}\left({y}\in \left\{{A},{B}\right\}\to {x}\in {y}\right)↔\left(\left({y}={A}\to {x}\in {y}\right)\wedge \left({y}={B}\to {x}\in {y}\right)\right)$
9 8 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B}\right\}\to {x}\in {y}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}={A}\to {x}\in {y}\right)\wedge \left({y}={B}\to {x}\in {y}\right)\right)$
10 1 clel4 ${⊢}{x}\in {A}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\to {x}\in {y}\right)$
11 2 clel4 ${⊢}{x}\in {B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={B}\to {x}\in {y}\right)$
12 10 11 anbi12i ${⊢}\left({x}\in {A}\wedge {x}\in {B}\right)↔\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\to {x}\in {y}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={B}\to {x}\in {y}\right)\right)$
13 3 9 12 3bitr4i ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B}\right\}\to {x}\in {y}\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
14 vex ${⊢}{x}\in \mathrm{V}$
15 14 elint ${⊢}{x}\in \bigcap \left\{{A},{B}\right\}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B}\right\}\to {x}\in {y}\right)$
16 elin ${⊢}{x}\in \left({A}\cap {B}\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
17 13 15 16 3bitr4i ${⊢}{x}\in \bigcap \left\{{A},{B}\right\}↔{x}\in \left({A}\cap {B}\right)$
18 17 eqriv ${⊢}\bigcap \left\{{A},{B}\right\}={A}\cap {B}$