# Metamath Proof Explorer

## Theorem inab

Description: Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion inab ${⊢}\left\{{x}|{\phi }\right\}\cap \left\{{x}|{\psi }\right\}=\left\{{x}|\left({\phi }\wedge {\psi }\right)\right\}$

### Proof

Step Hyp Ref Expression
1 sban ${⊢}\left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)↔\left(\left[{y}/{x}\right]{\phi }\wedge \left[{y}/{x}\right]{\psi }\right)$
2 df-clab ${⊢}{y}\in \left\{{x}|\left({\phi }\wedge {\psi }\right)\right\}↔\left[{y}/{x}\right]\left({\phi }\wedge {\psi }\right)$
3 df-clab ${⊢}{y}\in \left\{{x}|{\phi }\right\}↔\left[{y}/{x}\right]{\phi }$
4 df-clab ${⊢}{y}\in \left\{{x}|{\psi }\right\}↔\left[{y}/{x}\right]{\psi }$
5 3 4 anbi12i ${⊢}\left({y}\in \left\{{x}|{\phi }\right\}\wedge {y}\in \left\{{x}|{\psi }\right\}\right)↔\left(\left[{y}/{x}\right]{\phi }\wedge \left[{y}/{x}\right]{\psi }\right)$
6 1 2 5 3bitr4ri ${⊢}\left({y}\in \left\{{x}|{\phi }\right\}\wedge {y}\in \left\{{x}|{\psi }\right\}\right)↔{y}\in \left\{{x}|\left({\phi }\wedge {\psi }\right)\right\}$
7 6 ineqri ${⊢}\left\{{x}|{\phi }\right\}\cap \left\{{x}|{\psi }\right\}=\left\{{x}|\left({\phi }\wedge {\psi }\right)\right\}$