# Metamath Proof Explorer

## Theorem inrab

Description: Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006)

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

### Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
2 df-rab ${⊢}\left\{{x}\in {A}|{\psi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}$
3 1 2 ineq12i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cap \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}$
4 df-rab ${⊢}\left\{{x}\in {A}|\left({\phi }\wedge {\psi }\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)\right\}$
5 inab ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cap \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}=\left\{{x}|\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({x}\in {A}\wedge {\psi }\right)\right)\right\}$
6 anandi ${⊢}\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({x}\in {A}\wedge {\psi }\right)\right)$
7 6 abbii ${⊢}\left\{{x}|\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)\right\}=\left\{{x}|\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({x}\in {A}\wedge {\psi }\right)\right)\right\}$
8 5 7 eqtr4i ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cap \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)\right\}$
9 4 8 eqtr4i ${⊢}\left\{{x}\in {A}|\left({\phi }\wedge {\psi }\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\cap \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}$
10 3 9 eqtr4i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\cap \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }\wedge {\psi }\right)\right\}$