# Metamath Proof Explorer

## Theorem rabrab

Description: Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017)

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

### Proof

Step Hyp Ref Expression
1 rabid ${⊢}{x}\in \left\{{x}\in {A}|{\phi }\right\}↔\left({x}\in {A}\wedge {\phi }\right)$
2 1 anbi1i ${⊢}\left({x}\in \left\{{x}\in {A}|{\phi }\right\}\wedge {\psi }\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)$
3 anass ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)↔\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)$
4 2 3 bitri ${⊢}\left({x}\in \left\{{x}\in {A}|{\phi }\right\}\wedge {\psi }\right)↔\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)$
5 4 abbii ${⊢}\left\{{x}|\left({x}\in \left\{{x}\in {A}|{\phi }\right\}\wedge {\psi }\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)\right\}$
6 df-rab ${⊢}\left\{{x}\in \left\{{x}\in {A}|{\phi }\right\}|{\psi }\right\}=\left\{{x}|\left({x}\in \left\{{x}\in {A}|{\phi }\right\}\wedge {\psi }\right)\right\}$
7 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\}$
8 5 6 7 3eqtr4i ${⊢}\left\{{x}\in \left\{{x}\in {A}|{\phi }\right\}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }\wedge {\psi }\right)\right\}$