# Metamath Proof Explorer

## Theorem elin

Description: Expansion of membership in an intersection of two classes. Theorem 12 of Suppes p. 25. (Contributed by NM, 29-Apr-1994)

Ref Expression
Assertion elin ${⊢}{A}\in \left({B}\cap {C}\right)↔\left({A}\in {B}\wedge {A}\in {C}\right)$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in \left({B}\cap {C}\right)\to {A}\in \mathrm{V}$
2 elex ${⊢}{A}\in {C}\to {A}\in \mathrm{V}$
3 2 adantl ${⊢}\left({A}\in {B}\wedge {A}\in {C}\right)\to {A}\in \mathrm{V}$
4 eleq1 ${⊢}{x}={y}\to \left({x}\in {B}↔{y}\in {B}\right)$
5 eleq1 ${⊢}{x}={y}\to \left({x}\in {C}↔{y}\in {C}\right)$
6 4 5 anbi12d ${⊢}{x}={y}\to \left(\left({x}\in {B}\wedge {x}\in {C}\right)↔\left({y}\in {B}\wedge {y}\in {C}\right)\right)$
7 eleq1 ${⊢}{y}={A}\to \left({y}\in {B}↔{A}\in {B}\right)$
8 eleq1 ${⊢}{y}={A}\to \left({y}\in {C}↔{A}\in {C}\right)$
9 7 8 anbi12d ${⊢}{y}={A}\to \left(\left({y}\in {B}\wedge {y}\in {C}\right)↔\left({A}\in {B}\wedge {A}\in {C}\right)\right)$
10 df-in ${⊢}{B}\cap {C}=\left\{{x}|\left({x}\in {B}\wedge {x}\in {C}\right)\right\}$
11 6 9 10 elab2gw ${⊢}{A}\in \mathrm{V}\to \left({A}\in \left({B}\cap {C}\right)↔\left({A}\in {B}\wedge {A}\in {C}\right)\right)$
12 1 3 11 pm5.21nii ${⊢}{A}\in \left({B}\cap {C}\right)↔\left({A}\in {B}\wedge {A}\in {C}\right)$